> 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.
> 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.
Are there any good examples of where removing the leading "how" has improved the title? Or some list of title filtering rules with concrete examples of why they're implemented?
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.
> 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.
Title is missing the leading “How” from the source, which changes the meaning entirely.
Rehowed above.
Yup, the HN auto-filtering of titles often messes them up...
'How' is one of the most important conjunctive adverbs in the English language, and HN filters it out?
I'm just going to call that exactly as I see it - send the people writing these filtering rules back to middle school so they can learn basic English.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
Are there any good examples of where removing the leading "how" has improved the title? Or some list of title filtering rules with concrete examples of why they're implemented?
We don't keep track of that (too many things to keep track of) and I can't remember anything*. Sorry!
* https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...