Aliasing fun

[Robert Dewar]

<<Not quite, it's more like saying that it's hard to prove a set of
programs with some set of properties halts, because in general the
halting problem is undecidable.
>>

And this is false.

You seem to have a very odd idea of what undecidability is about, you seem
to treat it as some kind of cancer that send you running for the hills.

The fact that problem P (which you are not interested in solving) is
undecidable has no influence on the difficulty of proving some other
problem Q.

Obviously if Q is itself undecidable, then OK, you can't prove it but that
had nothing to do per se with the fact that P is undecidable.

So let's take the case from the quote above.

Yes, yes, we know from any undergraduate course in computing theory that
the general halting problem is undecidable -- very interesting bla bla.

But we are being asked to prove that a given subset of programs halts. Now
the fact that it is a subset means that the general result of undecidability
does not apply.

We have to look at this problem of the given subset as a completely different
problem, and whether or not a proof is possible in this case has nothing
whatever to do with the general problem.

For example, if I restrict programs to primitive recursion, and make certain
other restrictions on use of storage, it may be easy to prove termination for
the class. All the time we do total correctness proofs that prove termination.
It is not that such proofs are inherently easy or hard, or possible or
impossible, it varies with the case, but the fact that we can't solve the
general halting problem is not relevant.