🚀 go-pugleaf

In article <30095@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:
>But, if you want to say that Turing's theorem, or Herbrands theorem,
>or Fermats theorem tells us that type checking real programs is 
>impossible, then you don't understand any of these theorems ( or you've
>figured out something that it would be interesting to hear about).

If type safety is a property of *programs*, you can't let your answer
depend on the size of the machine running the program.  This forces you 
to use the TM model!

If you want to let "type safety" depend on what compiler and machine you're 
using, fine, but please realize that you're saying more about the machine
configuration than about the program you're supposed to be analyzing.
If adding one bit's worth of state space can change the answer you get, I 
claim that this notion of "type safety" is useless.

Your reasoning seems to go like this:

1. To run a program, one must use a physically realizable machine.
2. Real machines are only equivalent to FSMs.
3. Therefore, programs aren't REALLY equivalent to Turing machines.   
4. Since programs are not equivalent to TM's, we *can* solve the halting
   problem, do rigorous type checking,  etc...

No one is disputing (1) or (2).  You get into trouble with (3) though,
because programs and programming languages are mathematical abstractions.
We can reason about properties of programs without having to actually run 
them on a real machine, much as we can reason about the properties of 
integers without having to write them down on a real sheet of paper.

If we accept step (3) in your reasoning, then it follows that there are
REALLY only a finite number of prime numbers, since we don't have to
consider the ones that are too large to write down on any real sheet
of paper...sorry, Euclid!  

-- Jim Lewis
   U.C. Berkeley