From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
To: David McClain <David.McClain@Avisere.com>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Formal Methods
Date: Fri, 1 Oct 2004 09:36:08 +0200 [thread overview]
Message-ID: <16733.2280.350656.716714@gargle.gargle.HOWL> (raw)
In-Reply-To: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com>
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
next prev parent reply other threads:[~2004-10-01 7:36 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2004-09-30 15:51 David McClain
2004-09-30 17:35 ` Jacques Carette
2004-09-30 18:42 ` Jon Harrop
2004-10-01 8:24 ` Thomas Fischbacher
2004-10-01 9:01 ` Achim Blumensath
2004-09-30 17:54 ` [Off-topic] " David MENTRE
2004-10-01 7:36 ` Jean-Christophe Filliatre [this message]
2004-10-01 7:51 ` Tom
2004-10-01 9:04 ` Martin Berger
2004-10-01 8:30 ` Hendrik Tews
2004-10-01 9:18 ` Martin Berger
2004-09-30 17:19 Harrison, John R
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=16733.2280.350656.716714@gargle.gargle.HOWL \
--to=jean-christophe.filliatre@lri.fr \
--cc=David.McClain@Avisere.com \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox