[Prev][Next][Index][Thread]

Re: type safety

   On Mon, 10 Jan 2000, Joe Wells wrote:

   >   type safety: safety (for one program or for an entire programming
   >     language) enforced by requiring well typedness in some type
   >     system.
   > ...
   >   * Some people might define safety to also require the absence of
   >     uncatchable exceptions.  However, as long as these
   >     uncatchable exceptions generate well defined behavior (e.g.,
   >     halting), I think it is better to consider them safe.

        Joe, I infer from these statements, together with the fact
   that we can't tell at compile time whether an array index is in
   bounds, that any language which does not check array bounds
   dynamically cannot be type-safe.  Is my inference correct?  If not,
   how are such languages handled in your view?

There are a few points which need to be made in response to this.

1. It is not so clear that it is a "fact that we can't tell at compile
   time whether an array index is in bounds".  While it is undecidable
   in general whether a particular program will use an out-of-bounds
   array index (by a simple reduction from the halting problem), we
   can tell for many programs whether this is the case.

   Furthermore, various type systems can be designed which can
   represent proofs that out-of-bound array indexes are not used.
   These type systems can guarantee programs only use in-bounds
   indexes when accessing arrays.  The papers mentioned earlier by
   Hongwei Xi describe such type systems.  It is possible using such a
   type system to have safety without dynamic array bounds checks.

   The difficulties of course are that (1) these type systems tend to
   be complicated and (2) they can not handle some safe programs.

2. A language which does not verify (whether statically or dynamically)
   that array indexes are in bounds is not safe at all.

3. Consider a programming language PL which does not dynamically
   verify that array indexes are in bounds.  Let "sub" be the operator
   of PL such that sub(A,I) evaluates to the Ith element of array A,
   if 0 <= I < length(A), and otherwise has undefined behavior when
   evaluated (e.g., returns strange value, core dumps due to bus
   error, runs lethal electric current through the nearest keyboard,
   launches nearest nuclear-warhead-tipped missile, etc.).

   The important question now is:  What is the type of "sub"?  Suppose
   PL's type system assigns the following type to "sub":

     sub : forall 'a . ('a array * int) -> 'a

   This forall-quantified type can be instantiated, replacing 'a by
   any other type.  If this is the type of "sub", then this implies
   that the meaning of _every_ type (any type that can be substituted
   for 'a) includes "can have any behavior".  Hence no types of PL
   guarantee safety if the above type is used for "sub".

   In order for PL to have a type system that guarantees safety, it
   will need to give "sub" a more precise type, which rules out any of
   the argument pairs for which the behavior of "sub" is undefined.

-- 
Joe Wells
http://www.cee.hw.ac.uk/~jbw/
References: