Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: RE: reference initialization
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-05-16 (02:07)
From: Patrick M Doane <patrick@w...>
Subject: Re: RE: reference initialization
On Mon, 15 May 2000 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:

Patrick Doane