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 JAA12658; Fri, 1 Oct 2004 09:50:37 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA12250 for ; Fri, 1 Oct 2004 09:50:36 +0200 (MET DST) Received: from oceanite.ens-lyon.fr (oceanite.ens-lyon.fr [140.77.1.22]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i917oa1Y030039 for ; Fri, 1 Oct 2004 09:50:36 +0200 Received: from localhost (oceanite.ens-lyon.fr [127.0.0.1]) by oceanite.ens-lyon.fr (Postfix) with ESMTP id 61A5F320178 for ; Fri, 1 Oct 2004 09:50:08 +0200 (CEST) Received: from oceanite.ens-lyon.fr ([127.0.0.1]) by localhost (oceanite [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 04124-02 for ; Fri, 1 Oct 2004 09:50:08 +0200 (CEST) Received: from paille (unknown [140.77.13.92]) by oceanite.ens-lyon.fr (Postfix) with ESMTP id 4196332013E for ; Fri, 1 Oct 2004 09:50:08 +0200 (CEST) Received: from thirscho by paille with local (Exim 3.36 #1 (Debian)) id 1CDICT-0002jU-00 for ; Fri, 01 Oct 2004 09:51:33 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Message-ID: <16733.3205.309696.826268@gargle.gargle.HOWL> Date: Fri, 1 Oct 2004 09:51:33 +0200 To: caml-list@inria.fr Subject: Re: [Caml-list] Formal Methods In-Reply-To: <16733.2280.350656.716714@gargle.gargle.HOWL> References: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> <16733.2280.350656.716714@gargle.gargle.HOWL> X-Mailer: VM 7.18 under Emacs 21.3.1 Reply-To: Tom.Hirschowitz@ens-lyon.fr From: Tom X-Virus-Scanned: by amavisd-new-20030616-p10 (Debian) at ens-lyon.fr X-Miltered: at nez-perce with ID 415D0C4C.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 hirschowitz:01 ens-lyon:01 filliatre:01 mcclain:01 debugging:01 squares:01 haskell:01 pearls:01 equational:01 haskell:01 bug:01 higher-order:01 filliatre:01 lri:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk An example of formal methods applied to traditional imperative programming is the proof of a full copying garbage collector, using separation logic, by Birkedal et al: http://www.itu.dk/people/noah/papers/gc-popl.ps Jean-Christophe Filliatre writes: >=20 > David McClain writes: > > I have just been reviewing some papers by Greg Chaitin on Algorit= hmic=20 > > Complexity Theory, in which he boldly states that > >=20 > > "Similarly, proving correctness of software using formal methods = is=20 > > hopeless. Debugging is done experimentally, by trial and error. A= nd=20 > > cautious managers insist on running a new system in parallel with= the=20 > > old one until they believe that the new system works." > >=20 > > I wonder, as a non-specialist in this area, how the goals of FPL=20= > > squares with this result=3F >=20 > Proving a purely functional code is definitely easier than proving = an > imperative one; you'll find several projects to verify Haskell co= de > (such as OGI's Programatica) and many JFP Functional Pearls whe= re > equational reasoning is applied to Haskell code to prove = it > correct. You can also use the logic of a proof assistant to enco= de > directly purely functional programs and prove them correct (f= or > instance the OCaml library Set has been proved correct using the C= oq > proof assistant; and a small bug was found during the formal proof, = so > you can't say ``using formal methods is hopeless''). >=20 > The real difficulties in proving functional code appear wh= en > side-effects are mixed with powerful features such as polymorphism = or > higher-order. Then it becomes very hard to reason about program= s. > Actually, we don't even have a specification language to wri= te > programs properties to be proved. There is a nice challenge f= or > research here. >=20 > (Regarding more traditional imperative programming languages, I mu= st > disagree with Chaitin's statement: formal methods are more and mo= re > 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 ve= ry > small number of highly critical softwares.) >=20 > --=20 > Jean-Christophe Filli=E2tre (http://www.lri.fr/~filliatr) >=20 > ------------------- > To unsubscribe, mail caml-list-request@inria.fr Archives: http://cam= l.inria.fr > Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inr= ia.fr/FAQ/ > Beginner's list: http://groups.yahoo.com/group/ocaml=5Fbeginners ------------------- 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