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