GoKawiilHow I came to write THAT paper with Leslie Lamport
As people grow older, they grow wiser, or at least they think they do. Then it becomes their duty to impart their accumulated wisdom to the younger generation. Leslie Lamport made his name in distributed systems and fault tolerance. For many he is better known as the author of LaTeX, the famous macro package that makes Donald Knuth’s legendary TeX typesetting system usable for the rest of us. As Leslie grew older, he felt impelled to write a series of fairly wacky papers with titles such as “How to Write a Long Formula”. Another of these papers was called “Types Considered Harmful”, a diatribe against types in specification languages. Its title was an echo of a famous letter, “go to statement considered harmful”, by Edsger Dijkstra. The title of that letter (chosen by the journal editor) was subsequently borrowed by many authors who were against lots of things. Leslie was against types. But how did I get involved?
Types considered harmful
Leslie‘s thesis was that specification languages should be based on an untyped formalism (a sort of set theory) as opposed to a typed formalism. He advanced several arguments in favour: that untyped formalisms were more flexible; that typed formalisms raised numerous anomalies and issues; that what we would view as a type error in a specification would be detected anyway during verification.
There was some sense in this thesis. Type systems were in a state of flux in 1992 when that note was written. Coq (now Rocq) had only just appeared, and big changes were happening to Martin-Löf type theory. As for simple type theories, early implementations of HOL had been around only for a couple of years. It wasn’t clear what any typed calculus could do. Proof assistants did not yet support type classes. John Harrison was years away from introducing his trick to get low-budget dependent types, which works well enough to express $T^n$.
On the other hand, Lamport’s note was a mess. He seemed to be unfamiliar with any actual typed formalism and devoted most of his note to knocking down straw men. So when he submitted his note to TOPLAS for publication and it reached me to referee, my verdict was to reject. The other referee, David McAllester, reached the same verdict. That should’ve been that, but the editor, Andrew Appel, had other ideas.
“Put lipstick on it”
Debate is good, he said. These ideas deserve airing, or something of that sort. But we can’t allow errors in TOPLAS. Why don’t you join with Lamport as co-authors and transform the paper into something technically accurate but in the same spirit? I was game: I knew a fair bit about type systems and I also had my own untyped set-theoretic formalism (Isabelle/ZF), which I was happy to promote. David went along for a bit but soon dropped out. He was smart.
Leslie and I worked on the paper for a good while. It was a weird form of unwilling co-authorship, but somehow we managed. The new paper captured the core of Leslie‘s thesis while including a saner description of how types worked. Along the way, I witnessed Leslie’s unrivalled TeX mastery: low-level tricks that I have never encountered since.
A second round of review, oh God
... continue reading