This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: Aliasing fun
- From: Daniel Berlin <dan at dberlin dot org>
- To: Robert Dewar <dewar at gnat dot com>
- Cc: gcc at gcc dot gnu dot org
- Date: Fri, 25 Jan 2002 12:36:10 -0500 (EST)
- Subject: Re: Aliasing fun
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