🚀 go-pugleaf

In article <1991May6.021753.4373@agate.berkeley.edu> jwl@sag4.ssl.berkeley.edu (Jim Lewis) writes:
>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.
>

That's a good point, but there are really two different issues. If
you give me a sorting algorithm A so that A(sequence ) -> sorted-sequence
I really want to know if A is correct on every sequence, and 
knowing A(sequences-representable-on-a-TRS-80) is not very satisfactory.
But, it is often of interest to know if an algorithm can be sensibly
compiled on a real machine. Thus, if our compiler provides a sorting
algorithm, and we attempt to compile a program 
which applies the sorting operator to a sequence that cannot be sorted
on our machine, then it would be both useful and theoretically
possible to have the compiler find and report the error.
So, maybe we don't have an algorithm that will decide if our program is
type-safe on all possible computers -- i.e.
we can't decide (forall Machine)TypeSafe(Prog, Machine), but maybe we 
we can have an algorithm that will decide for any given  machine
if the program is typesafe --- i.e. maybe there is an algorithm
that will decide TypeSafe(Prog,Machine)  for every Machine.  Maybe
we can even do better than that, and have an algorithm that 
will compute TypeSafe(Prog,Bound) so that any machine M that fits
within the Bound is typesafe. If our compiler could test
TypeSafe(Prog,Anything-with-at-least-2^32-addressable-words)
this would would be quite useful.
Remember that while $(forall x)f(x)=0$ is not decidable for
arbitrary primitive recursive function f,  for every integer n, 
$f(n)=0$ is decidable. I'm certainly not arguing that we should
dispense with unbounded quantifiers in ordinary mathematical 
discourse (although some folks do, see Nelson, Predicative Arithmetic, for
example). But I am arguing that in computer engineering, where we often
would find it more interesting to know if Prog is type safe on 
the set of all computers made inthe last 10 years (a decidable question)
than if there is a hypothetical  computer on which Prog is not typesafe
(not decidable for any decent programming language), we should be a little
more careful about invoking Turing's theorem.