[Prev][Next][Index][Thread]
Re: type safety
-
To: Jon Fairbairn <Jon.Fairbairn@cl.cam.ac.uk>
-
Subject: Re: type safety
-
From: Corky Cartwright <cork@rice.edu>
-
Date: Thu, 30 Dec 1999 06:25:36 -0600 (CST)
-
cc: types@cis.upenn.edu
-
In-Reply-To: <199912292250.RAA07235@localhost.localdomain>
-
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
terminate.
-- Corky Cartwright