🚀 go-pugleaf

In article <1991May9.205401.12382@auto-trol.com> davgot@auto-trol.com (David Gottner) writes:

|PRACTICAL computers may be FSM's but programming languages are not.  Nowhere
|in the ANSI C standard does it give a maximum amount of memory that a C
|program can run in.  Thus your program checker must assume that the program
|that it is analyzing will never run out of tape, which means that the analyzer
|must assume that the program will run on a Turing Machine, and the 
|undecidability theorem applies.

I never disagreed. But.

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.

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).

But frankly, I think I'd rather have that flagged as an error, even if
that's technically wrong! (Not that this invalidates your point.)

Honestly I didn't think this was what we were talking about....
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
systems analyst                                  University of Chicago
----------------------------------------------------------------------