English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] Formal Methods
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-09-30 (15:51)
From: David McClain <David.McClain@A...>
Subject: [Caml-list] Formal Methods
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."

from

http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html

He goes to great lengths to discuss the halting problem and its 
implications for proving correctness of algorithms.

I wonder, as a non-specialist in this area, how the goals of FPL 
squares with this result?

David McClain
Senior Corporate Scientist
Avisere, Inc.

david.mcclain@avisere.com
+1.520.390.7738 (USA)