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.
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.
In general, any of these properties can be checked statically, just like czwarich said. You have to be conservative, but that's not any different than a type system, or Rust's borrow checker. There are certainly languages that enforce termination, and you can design systems that enforce higher-level progress properties (such as absence of deadlock).
The major difference between a liveness property and the other kind (called a safety property: at no point does this bad thing happen) is that you can't check for liveness properties dynamically.