Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- Title is missing the leading “How” from the source, which changes the meaning entirely.by blltprfmnk
- Yup, the HN auto-filtering of titles often messes them up...by Hunpeter
- Rehowed above.by dang
- > 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.
by mrkeen - > 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.
Yup, TLA+ is a totally different beast from, say, Lean 4. Both are useful. I don't want dependent types in TLA+ either.
by erichocean - > The other referee, David McAllester, reached the same verdict.
The same David McAllester who introduced PAC-Bayesian bounds ?
Ans: Yes.
by srean - Somehow the final version of the paper is not linked from the blog post: https://www.microsoft.com/en-us/research/publication/specifi...by joomy