Version franēaise
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: -- (:)
From: Tom <tom.hirschowitz@e...>
Subject: Re: [Caml-list] Formal Methods

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:

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 (
 > -------------------
 > To unsubscribe, mail Archives:
 > Bug reports: FAQ:
 > Beginner's list:

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: