4 ms·
Statically checking that progress is made does imply that the language is not Turing-complete if I understand it correctly, which is why Coq, the proof assistan
by heinrich5991 11y ago
Statically checking that progress is made does imply that the language is not Turing-complete if I understand it correctly, which is why Coq, the proof assistant language where all programs have to terminate, is not Turing-complete.
- samth 11y agoThis is not correct. It's possible to write a sound static checker for termination of a Turing complete language. There are some terminating programs on which it will have to say "I don't know", however.
- kibwen 11y agoThis is my understanding as well, and underlies my assertions above. After all, if a compiler can tell you for certain that any given program written in a Turing-complete language will terminate, then you've literally just solved the halting problem. :P
- TheCoelacanth 11y agoOf course, it's true that it can't be proven whether any arbitrary program will halt or not, but in practice most (possibly all) useful programs can be proven to halt or not halt.