English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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 (08:22)
From: Markus Mottl <mottl@m...>
Subject: Re: RE: reference initialization
> 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:


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