3 ms·
> Which, y'know, good luck with that. Most dependent type systems like Agda, Coq, Idris, Lean, and ATS have termination checking, so it is possible! They can't
by bjz_ 9y ago
> Which, y'know, good luck with that.
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.
- noblethrasher 9y agoSince 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.
- geokon 9y agoNow you've got me curious :) Could you give some examples? I've never come across regular expressions outside of string handling