Re: type safety
To: Jon Fairbairn <Jon.Fairbairn@cl.cam.ac.uk>
Subject: Re: type safety
From: Corky Cartwright <email@example.com>
Date: Thu, 30 Dec 1999 06:25:36 -0600 (CST)
References: <199912291950.OAA06972@localhost.localdomain> <199912292250.RAA07235@localhost.localdomain>
>> 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