From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA07431 for caml-redist@pauillac.inria.fr; Tue, 16 May 2000 10:22:05 +0200 (MET DST) Resent-Message-Id: <200005160822.KAA07431@pauillac.inria.fr> Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id AAA32454 for ; Tue, 16 May 2000 00:31:46 +0200 (MET DST) Received: from miss.wu-wien.ac.at (miss.wu-wien.ac.at [137.208.107.17]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e4FMVkT23576 for ; Tue, 16 May 2000 00:31:46 +0200 (MET DST) Received: (from mottl@localhost) by miss.wu-wien.ac.at (8.9.0/8.9.0) id AAA17997; Tue, 16 May 2000 00:31:43 +0200 (MET DST) From: Markus Mottl Message-Id: <200005152231.AAA17997@miss.wu-wien.ac.at> Subject: Re: RE: reference initialization To: bdb-as-camluser@netcourrier.com Date: Tue, 16 May 2000 00:31:43 +0200 (MET DST) Cc: caml-list@inria.fr (OCAML) In-Reply-To: from "bdb-as-camluser@netcourrier.com" at May 15, 2000 03:43:11 PM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Resent-From: weis@pauillac.inria.fr Resent-Date: Tue, 16 May 2000 10:22:05 +0200 Resent-To: caml-redist@pauillac.inria.fr > 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