From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id XAA24020 for caml-redist@pauillac.inria.fr; Mon, 15 May 2000 23:01:30 +0200 (MET DST) Resent-Message-Id: <200005152101.XAA24020@pauillac.inria.fr> Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA01126 for ; Mon, 15 May 2000 15:44:42 +0200 (MET DST) Received: from front4.grolier.fr (front4.grolier.fr [194.158.96.54]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e4FDigP21944 for ; Mon, 15 May 2000 15:44:42 +0200 (MET DST) Received: from netc-1v.grolier.fr (netc-1v.grolier.fr [194.158.97.217]) by front4.grolier.fr (8.9.3/No_Relay+No_Spam_MGC990224) with ESMTP id PAA02975; Mon, 15 May 2000 15:44:39 +0200 (MET DST) From: bdb-as-camluser@netcourrier.com Received: (from mnet@localhost) by netc-1v.grolier.fr (8.9.3/8.9.3) id PAA16060; Mon, 15 May 2000 15:43:11 +0200 (MET DST) Date: Mon, 15 May 2000 15:43:11 +0200 (MET DST) To: sweirich@cs.cornell.edu Cc: caml-list@inria.fr Subject: Re: RE: reference initialization X-Mailer: Medianet/v1.13 Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Resent-From: weis@pauillac.inria.fr Resent-Date: Mon, 15 May 2000 23:01:30 +0200 Resent-To: caml-redist@pauillac.inria.fr Hello, sweirich=40cs.cornell.edu wrote: ) type 'a ptr =3D a' option ref ) exception NullPointer ) let new () =3D ref None ) let get x =3D match =21x with Some y -> y =7C None -> raise NullPointer ) let set x y =3D x :=3D 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 =5FJava=5F i= s ) 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, i= sn't it? To me, neither approach (ML/Java/C) is satisfying. I have the strong feeli= ng that the =5Fonly=5F way that maximum efficiency and safeness can be ach= ieved is to let the programmer specify =5Fproofs=5F 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 saf= eness (regardless of fitness for a particular purpose) of the program he i= s writing, and let the compiler use these proofs? Beno=EEt de Boursetty. ----- La messagerie itin=E9rante sans abonnement NetCourrier ----- Web : www.netcourrier.com Minitel : 3615 et 3623 NETCOURRIER T=E9l : 08 36 69 00 21