4 ms·
A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove
by _vdpp 4y ago
A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.
- kaba0 4y agoYou forget about Rice’s theorem. Termination is not that exciting, but the existence of race conditions and a million other properties are - and those are not possible to prove true in general.
- ebingdom 4y agoNo, docandrew is correct. You are incorrectly applying Rice's theorem. Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.
- deleted 4y ago[deleted]
- User23 4y agoWe have general methods for constructing programs that have some desired property, such as termination. We have no general methods for finding whether or not some arbitrary program has some desired property, such as termination.
- Tainnor 4y agoI agree in general and also take issue with the "we can never prove interesting things about our programs" statements that are sometimes uttered, but it is surprisingly easy to write certain programs that nobody to this date knows whether they terminate, such as: "find the least even number > 2 that cannot be written as the sum of two primes". :)