From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA09259; Fri, 1 Oct 2004 09:36:10 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 JAA12167 for ; Fri, 1 Oct 2004 09:36:09 +0200 (MET DST) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i917a8K9026486 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Fri, 1 Oct 2004 09:36:09 +0200 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id D972919E721; Fri, 1 Oct 2004 09:36:08 +0200 (CEST) Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 14303-08; Fri, 1 Oct 2004 09:36:08 +0200 (CEST) Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id C5E2C19E719; Fri, 1 Oct 2004 09:36:08 +0200 (CEST) Received: from pc8-142 (pc8-142 [129.175.8.142]) by smtp.lri.fr (Postfix) with ESMTP id 4EF0CCEE10; Fri, 1 Oct 2004 09:36:08 +0200 (CEST) Received: from filliatr by pc8-142 with local (Exim 3.36 #1 (Debian)) id 1CDHxY-0000Wc-00; Fri, 01 Oct 2004 09:36:08 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Message-ID: <16733.2280.350656.716714@gargle.gargle.HOWL> Date: Fri, 1 Oct 2004 09:36:08 +0200 To: David McClain Cc: caml-list@inria.fr Subject: Re: [Caml-list] Formal Methods In-Reply-To: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> References: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> X-Mailer: VM 7.18 under Emacs 21.3.1 From: Jean-Christophe Filliatre X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at concorde with ID 415D08E8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 filliatre:01 filliatre:01 lri:01 mcclain:01 debugging:01 squares:01 haskell:01 pearls:01 equational:01 haskell:01 bug:01 higher-order:01 lri:01 filliatr:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk David McClain writes: > I have just been reviewing some papers by Greg Chaitin on Algorithmic > Complexity Theory, in which he boldly states that > > "Similarly, proving correctness of software using formal methods is > hopeless. Debugging is done experimentally, by trial and error. And > cautious managers insist on running a new system in parallel with the > old one until they believe that the new system works." > > I wonder, as a non-specialist in this area, how the goals of FPL > squares with this result? Proving a purely functional code is definitely easier than proving an imperative one; you'll find several projects to verify Haskell code (such as OGI's Programatica) and many JFP Functional Pearls where equational reasoning is applied to Haskell code to prove it correct. You can also use the logic of a proof assistant to encode directly purely functional programs and prove them correct (for instance the OCaml library Set has been proved correct using the Coq proof assistant; and a small bug was found during the formal proof, so you can't say ``using formal methods is hopeless''). The real difficulties in proving functional code appear when side-effects are mixed with powerful features such as polymorphism or higher-order. Then it becomes very hard to reason about programs. Actually, we don't even have a specification language to write programs properties to be proved. There is a nice challenge for research here. (Regarding more traditional imperative programming languages, I must disagree with Chaitin's statement: formal methods are more and more applied to critical software. But it requires a lot of work to formally verify a few lines of code, so it only applies to a very small number of highly critical softwares.) -- Jean-Christophe Filliātre (http://www.lri.fr/~filliatr) ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners