Re: Aliasing fun

[Daniel Berlin <dan at dberlin dot org>]

On Fri, 25 Jan 2002, Daniel Berlin wrote:

> 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
And before you bring up the class of programs that consist of only calling 
various exit functions, remember that in aliasing, the sets of properties 
are much more complex than that.

Trying to reason about type system aliasing seems to invariably 
lead people to restrict to subsets and be done with it, or start 
inventing/using logic systems of various sorts with known decidability  
properties, and they do this specifically to avoid dealing with 
decidability issues.

--Dan