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 KAA08349; Fri, 1 Oct 2004 10:30:18 +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 KAA15445 for ; Fri, 1 Oct 2004 10:30:17 +0200 (MET DST) Received: from tcs.inf.tu-dresden.de (tcs.inf.tu-dresden.de [141.76.75.101]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i918UGrd001257 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 1 Oct 2004 10:30:17 +0200 Received: from ithif59.inf.tu-dresden.de (ithif59 [141.76.75.59]) by tcs.inf.tu-dresden.de (8.12.9/8.12.9) with ESMTP id i918UDI6028785 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=NOT) for ; Fri, 1 Oct 2004 10:30:14 +0200 (MET DST) Received: from tews by ithif59.inf.tu-dresden.de with local (Exim 4.34) id 1CDInt-0005bR-8P for caml-list@inria.fr; Fri, 01 Oct 2004 10:30:13 +0200 To: caml-list@inria.fr Subject: Re: [Caml-list] Formal Methods References: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> From: Hendrik Tews Date: 01 Oct 2004 10:30:13 +0200 In-Reply-To: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> Message-ID: User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.3 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang) at tcs.inf.tu-dresden.de X-Miltered: at concorde with ID 415D1598.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 hendrik:01 tews:01 tews:01 mcclain:01 mcclain:01 seldom:01 squares:01 well-typed:01 side-effect:01 haskell:01 casts:01 hendrik:01 tu-dresden:01 tu-dresden: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. This is just nonsense. You can prove the correctness of any piece of software (provided it is correct). Its only some orders of magnitute more expensive than developing the same software, therefore proving correctness is seldom attempted in practice. Further the halting problem is just not relevant here. It only means that you can not hope for a fully automatic procedure. However, every decent programmer knows why his while loops terminate. So you just go and ask him and use his answer in your correctness proof. In general, software verification is not difficult, it is complex. I wonder, as a non-specialist in this area, how the goals of FPL squares with this result? If you have a well-typed programm for a language with a strong type system you can use a simpler semantics. Thus verification becomes cheaper. Now, if you have a side-effect free language, like Haskell, it becomes even more simpler and cheaper. However, nowadays a semantics exists even for quite dirty languages like Java, C or C++. You are not bound to functional programming if you want to use formal methods. Goto statements, pointer arithmetic and even type casts are not a problem if you use the right technology. Bye, Hendrik Tews (I am working in the VFiasco project that attempts to verify properties of the Fiasco micro-kernel written in C++. Checkout http://os.inf.tu-dresden.de/vfiasco/) ------------------- 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