Re: RE: reference initialization

From: Patrick M Doane (patrick@watson.org)
Date: Tue May 16 2000 - 04:06:37 MET DST

  • Next message: Dave Mason: "Re: reference initialization"

    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



    This archive was generated by hypermail 2b29 : Tue May 16 2000 - 04:12:47 MET DST