Re: RE: reference initialization

Re: RE: reference initialization

[bdb-as-camluser]

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

Re: RE: reference initialization

[Markus Mottl]

> 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?

It is indeed possible to have a type system that can be used (misused? ;)
to prove just about any property of your program - nearly...

A language that implements this is Cayenne:

  http://www.cs.chalmers.se/~augustss/cayenne

The type system of Cayenne is equivalent in power to predicate logic
(pretty expressive).  However, this expressiveness is bought with
decidability: it is, of course, impossible to automatically prove
everything without sometimes sending your type checker to Nirvana (or
worse: do something unsound)...

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: RE: reference initialization

[Patrick M Doane]

On Mon, 15 May 2000 bdb-as-camluser@netcourrier.com wrote:

> 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? 

You might want to take a look at work by George Necula for Proof Carrying
Code (PCC), in particular his Touchstone compiler.

One of the optimizations performed by the compiler is the removal of
null-pointer checks. In cases where the compiler does not have enough
local information to remove the check, a precondition can be written that
will be used during optimization.

More about the compiler and PCC in general can be found at his website:

http://www-nt.cs.berkeley.edu/home/necula/public_html/

Patrick Doane