David McClain <David.McClain@Avisere.com> 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