Re: type safety

[I understand that there are more powerful type theories than ML's and that
 we can built a much richer hierarchy of numeric types.]

Jon writes: 

  I aver that the standard simple type system _can_ eliminate 
  [C], although most language designs don't do this -- this 
  is a failure of will on the part of programming language 
  designers, not the type system

  > So, a program in this language may still signal an
  >    error: attempt to divide by 0. Call this an exception or whatever you
  >    will, it is a behavior that you don't want. 

  Even with a limited type system, you can make Integer an 
  abstract type uniting NZInteger and Zero

  divide then gets the type Integer -> NZInteger -> Integer.
  Of course, this requires the programme to be peppered with
  tests, ...

Right: if the original program looked like this: 

 (lambda (n : Integer)
  (/ 1 n))

yours will be 

 (lambda (n : Integer-Abstract-Type)
  (if (instanceof n Zero) 
      (error 'division-by-zero)
      (/ 1 (cast-to-NZInteger n))))

or something like this. And how is your type system going to prove to me
that (error 'division-by-zero) is never going to be called? By pushing
tests and error/exception signals into programs, you don't get any more
program safety than we had. 

-- Matthias