Somehow the final version of the paper is not linked from the blog post: https://www.microsoft.com/en-us/research/publication/specifi...

> The other referee, David McAllester, reached the same verdict.

The same David McAllester who introduced PAC-Bayesian bounds ?

Ans: Yes.

https://link.springer.com/article/10.1023/A:1007618624809

> 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.

Title is missing the leading “How” from the source, which changes the meaning entirely.