Re: Type safety on wikipedia

[Florian Weimer <fw@deneb.enyo.de>]

> Even with unchecked conversion Ada has the 'Valid attribute, allowing
> the programmer to determine if the result of an unchecked conversion is
> a valid value.

Only in very limited cases.

> I do not see how Unchecked_Deallocation interferes with type safety.

The following is just a rough sketch, but maybe it helps to clarify
the terms.

A type system gives you a subset of all expressions which are
well-typed (in Ada, 1 + 1 is well-typed, but 1.0 + 1 is not).

A type-safe language has a type system with these two properties: any
well-typed expression which is not a value can be reduced to a simpler
expression, according to a set of run-time evaluation rules (which
define the semantics of the language) -- and these simplification
steps preserve the well-typedness of expressions.

(Of course, considerable notational overhead is needed to apply this
definitions in a rigorous manner to real-world programming languages.)

Now, suppose that X is a pool-specific access value for some type T,
and Free is a corresponding instance of Ada.Unchecked_Deallocation.
Suppose that


   Free (X);

has just been exected.  Suppose the next thing to be evaluated is

   declare
      Y : T := X.all;
   begin
      ...

Now X.all is not a value, so it has to reduce (at run-time) to some
other expression.  But the language definition explicitly tells you
that no such rule exists.  Therefore, the first rule I mentioned is
violated, and Ada with Ada.Unchecked_Deallocation is not type-safe.