general type theory set theory memories 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
Meanwhile, Andrew Appel had stepped down as TOPLAS editor. The new editor, Carl Gunter, had not been informed about the special status of this paper. So when it reached him, he sent it to fresh referees. This was not part of the plan. And the new referees also decided to reject the paper. One of the reports was incoherent. It obviously had been written while its author was suffering a fit of apoplexy. So then I contacted Carl and said, wait a minute, my rejection is worth nothing and this guy‘s rejection is somehow valid? Plus, he’s literally insane. So the paper appeared after all, with a disclaimer expressing wishes for a lively debate, etc. etc. etc. I’m not sure the debate ever happened.
In retrospect
And now we can ask how well Leslie’s thesis holds up 27 years later. It’s fair to say, not so well. Type systems have evolved considerably and they have proved their worth in numerous specification and verification tasks, some on an industrial scale.
Meanwhile, little progress has been made on the issues that plague set-theoretic formalisms. Without types you don’t have overloading of notation, which is trivial in principle (you can just use lots of different symbols), but a big deal in practice. And worse, the ability to write absolutely anything is mostly an invitation to make mistakes. Verification is an extremely expensive way to find such mistakes, and those you do not find could render your proofs worthless. As far as I know, even Lamport’s own specification language (TLA+) was eventually implemented with some type restrictions.
So, in fact, your specification language probably should be typed. But it is also still worth looking for ways to make set-theoretic notations work better.