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