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