> 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