Re:Linear types can change the world (1990) [pdf]
by noblethrasher on Tuesday January 09, 2018 @06:18PM
(#16111099)
Since I've started paying attention, I've noticed that most of the code I write doesn't need anything more powerful than formal regular expressions, and vanishingly rarely needs to go beyond deterministic context-free.
Most dependent type systems like Agda, Coq, Idris, Lean, and ATS have termination checking, so it is possible! They can't determine whether arbitrary programs terminate, but you can capture a large subset of programs. Turns out most code doesn't actually need Turing completeness.