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:
 > 
 > 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

-------------------
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