Re:Why Rust? [pdf]
by heinrich5991 on Wednesday September 09, 2015 @04:15PM
(#10194230)
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.
[ Parent
| on HN ]
This 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
Re:Why Rust? [pdf]
by TheCoelacanth on Thursday September 10, 2015 @11:43AM
(#10198697)
Of 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.
This 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.