4 ms·
This is what's usually called a "liveness" property: eventually the system will do some particular thing. These two in particular are often called "progress" in
by samth 11y ago
This is what's usually called a "liveness" property: eventually the system will do some particular thing. These two in particular are often called "progress" in some contexts, but that's rarely formal.
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.
- heinrich5991 11y agoStatically 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.