🚀 go-pugleaf

In article <STEPHEN.91May10020459@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
>
>First of all, I would be more interested in a verifier that told me
>about what my programme would do *if compiled* than one that told me
>what it would do if run on a non-realisable machine.
>

You are right, a good verifier should be able to tell you approximately how much
time/space overhead a program will require.  (After all, humans can do this for
algorithms, so a verifier should be able to do so also)  

However suppose the verifier said "This program will not halt on a machine
with no more than 16 MB"  Well, we can get a 32MB machine and run it.  In
otherwords if the verifier can show the program works or doesn't work on
a machine with memory <= M, then we can run it on a machine with memory M+1.
Thus, there is really no way to avoid Turing undecideability.

>Secondly, your argument applies to languages as they are presently
>defined; personally I wouldn't BOTHER writing a verifier for C (though
>if I had one there are times when I'd use it). A *new* type system,
>for instance, might be able to get very good mileage out of the
>assumption that resources are finite (though I'd be very unhappy if it
>assumed any PARTICULAR bound, I think). I wouldn't know, of course;
>I'm no theorist.
>
>But I grant your point: a C programme could consume an unbounded
>amount of stack and still be correct by the standard (though it would
>take a VERY imaginative implementation to get the heap to contain
>more than ULONG_MAX distinct objects, whatever ULONG_MAX is).
>

I don't think I'd want to use a language that placed limits on the number
of active objects (unless it is a large limit like ULONG_MAX :-) )
-- 
David Gottner
davgot@auto-trol.COM                           Auto-trol Technology Corporation
{...}ncar!ico!auto-trol!younam                 12500 North Washington Street
(303) 252-2321                                 Denver, CO 80241-2404