How I came to write THAT paper with Leslie Lamport
Lawrence Paulson recounts how he ended up co-authoring a paper with Leslie Lamport, despite initially rejecting Lamport's note "Types Considered Harmful" as a referee. The paper, which argued against types in specification languages, was eventually published after a convoluted editorial process. Paulson reflects on the debate 27 years later, concluding that type systems have proven their worth in verification, while set-theoretic formalisms have struggled.
As people grow older, they grow wiser, or at least they think they do.
- joomy
Somehow the final version of the paper is not linked from the blog post: https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> The other referee, David McAllester, reached the same verdict.
The same David McAllester who introduced PAC-Bayesian bounds ?
Ans: Yes.
- mrkeen
> 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 Tn
I don't want to stick linear or dependent types into TLA+. Proving dynamic properties with an exhaustive runtime is a totally different game from what you might do statically.
But I do want to rule out nonsense. Sure, I can prove that traffic light never equals RED_LIGHT. Too bad if it equals RED.