> 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.
blltprfmnk 6 hours ago [-]
Title is missing the leading “How” from the source, which changes the meaning entirely.
Hunpeter 6 hours ago [-]
Yup, the HN auto-filtering of titles often messes them up...
lightedman 5 hours ago [-]
'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.
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?
dang 5 hours ago [-]
Rehowed above.
Rendered at 22:38:31 GMT+0000 (Coordinated Universal Time) with Vercel.
The same David McAllester who introduced PAC-Bayesian bounds ?
Ans: Yes.
https://link.springer.com/article/10.1023/A:1007618624809
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'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.