POPL
Last night, I returned from my very first POPL, very exhausted, and very satisfied. It was great putting faces to names, chatting with potential PhD supervisors (both from the US and in the UK), and reveling in the atmosphere.
Highlights from my files:
- Tony Hoare, on being awarded the ACM SIGPLAN Programming Languages Achievement Award, even though he has received so many other awards, “...it makes me feel a little guilty. I didn’t ask for it!”
- Hoare: “I like mistakes; if I find it’s my fault, I can rectify it. If it’s someone else’s fault, there’s not much you can do.”
- Hoare: “Simplicity is not an engineering goal.”
- Tony had just described how he retracted an accepted paper because the reasoning on it was intricate, and he didn’t think it presented program proving in a good light. The interviewer complimented him for his principles, saying that if he had a paper accepted which he didn’t think was up to snuff, he probably wouldn’t have the courage to retract it. It was “so brave.” To which Tony replies, “Well, I wish you could!” [laughter] “Unfortunately, the pressure to publish has increased. We feel obliged to publish every year, and the quality of the average paper is not improved.”
- One recurring theme: Tony Hoare mentioned that proofs and tests were not rivals, really they were just the same thing... just different. In the “Run your Research” talk, these theme came up again, where this time the emphasis was executable papers (the “run” in “Run your Research”).
- “Don’t just support local reasoning, demand it!” (Brute force proofs not allowed!)
- On JavaScript: “null is sort of object-y, while undefined is sort of primitive-y.”
- The next set come from the invited speaker from the computer networks community. “During 9/11, on average, the Internet was more stable. The reason for this was the NetOps went home.” (on the causes of network outages in practice.)
- “Cisco routers have twenty million lines of code: there’s actually an Ada interpreter in there, as well as a Lisp interpreter.”
- “It used to be acceptable to go down for 100ms... now we have video games.”
- Speaker: “I am the walrus.” (Goo goo g' joob.)
- “I believe we do not reuse theorems. We reuse proof methods, but not the actual theorems. When we write papers, we create very shallow models, and we don’t build on previous work. It’s OK. It’s the design. It doesn’t matter too much. The SML standard was distributed with a bug report, with 100+ mistakes in the original definition. Doesn’t detract from its impact.”
- “Put on the algebraic goggles.”
- “The Navy couldn’t install it [a system for detecting when classified words were being transmitted on insecure channels], because doing so would be admitting there was a mistake.”
- “Move to something really modern, like Scheme!” (It’s like investing one trillion, and moving from the thirteenth century to the fourteenth.)
- Strother Moore (co-creator of ACL2): “After retirement, I’ll work more on ACL2, and then I’ll die.”
- “What’s the best way to make sure your C program is conforming?” “Write deterministic code.” [laughter]