Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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,,