Re: type safety

>> 4. Types can never prove that all safety restrictions will be respected. 

>I don't beleive this to be true; For most type systems you 
>cannot guard against non-termination, but I don't think 
>anyone has ever claimed otherwise.  For type-theory based 
>languages, even that can be avoided.

Nonsense.  Consider the trivial issue of array bounds checking.  No
type system can assure all subscript expressions are in range; this
is a patently undecidable problem.

For that matter so is non-termination--unless a program contains an
embedded proof that it terminates, which is utterly impractical.
Moreover, many programs (interpreters, stream filters) do not always

-- Corky Cartwright