Hacker News Reader

Comment by _vdpp | Hacker News Reader

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.

View on HN

We 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.

I 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". :)

You 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.

No, 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.

Reply on news.ycombinator.com