Re: RE: reference initialization

From: Markus Mottl (mottl@miss.wu-wien.ac.at)
Date: Tue May 16 2000 - 00:31:43 MET DST

  • Next message: Xavier Leroy: "Re: The performance cost of using exceptions?"

    > 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
    



    This archive was generated by hypermail 2b29 : Tue May 16 2000 - 10:26:24 MET DST