Re: RE: reference initialization

[bdb-as-camluser@netcourrier.com]

Hello,

sweirich@cs.cornell.edu wrote:
) type 'a ptr = a' option ref
) exception NullPointer
) let new () = ref None
) let get x = match !x with Some y -> y | None -> raise NullPointer
) let set x y = x := Some y 
) 
) ML, of course, lacks the syntactic support to use these pointers as
) gracefully as Java can. On the other hand, the problem with _Java_ is
) efficiency loss, as the programmer cannot syntactically enforce that the
) reference is initialized -- requiring a null check at every use.

Well, I am sorry but 'get' is also performing a null check at every use, isn't it?

To me, neither approach (ML/Java/C) is satisfying. I have the strong feeling that the _only_ way that maximum efficiency and safeness can be achieved is to let the programmer specify _proofs_ of safeness when it is not obvious at the syntaxic or type level.

Are there any languages in which the programmer can indicate proofs of safeness (regardless of fitness for a particular purpose) of the program he is writing, and let the compiler use these proofs?

Benoît de Boursetty.

----- La messagerie itinérante sans abonnement NetCourrier -----
Web : www.netcourrier.com     Minitel : 3615 et 3623 NETCOURRIER
                  Tél : 08 36 69 00 21