Aliasing fun
Daniel Berlin
dan@dberlin.org
Fri Jan 25 10:21:00 GMT 2002
On Fri, 25 Jan 2002, Robert Dewar wrote:
> <<No, I mean what I said. It's hard to reason about formally, because in
> reasoning abuot it formally, undecidability is a significant issue.
> >>
>
> That's like saying it is hard to prove that a given program halts because
> in general the halting problem is undecidable. Such a statement would, as
> I hope you can understand, be utter nonsense.
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.
Which is, in actuality, true.
It *is* hard to prove that certain classes of programs always halt.
Precisely because we know that in general, we can't decide that for all
classes, and you need to show that somehow, your restricted subset makes
it possible to decide for *all* programs in that subset.
--Dan
More information about the Gcc
mailing list