From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id EAA19636; Tue, 16 May 2000 04:07:17 +0200 (MET DST) Received: from fledge.watson.org (fledge.watson.org [204.156.12.50]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e4G27GT28427; Tue, 16 May 2000 04:07:16 +0200 (MET DST) Received: from localhost (patrick@localhost) by fledge.watson.org (8.9.3/8.9.3) with SMTP id WAA14210; Mon, 15 May 2000 22:06:48 -0400 (EDT) (envelope-from patrick@watson.org) Date: Mon, 15 May 2000 22:06:37 -0400 (EDT) From: Patrick M Doane To: bdb-as-camluser@netcourrier.com cc: sweirich@cs.cornell.edu, caml-list@inria.fr, Pierre.Weis@inria.fr, caml-redist@pauillac.inria.fr Subject: Re: RE: reference initialization In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII 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