Re: [Caml-list] Formal Methods

[Martin Berger <martinb@dcs.qmul.ac.uk>]

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

it is a bit more complicated than that. it seems to be the case, and
maybe that's what chaitin is getting at, that the more complicated
the program under verification and the more complicated the property
to be established, the more that verification is like writing a program.
but then the question "is the specification correct?" becomes as hard
as, or identical with "has the program that property?". so in the limit
there seems to be a real problem in that we can trust  verification
only in as much as we can trust programming.

BUT, and that's a very big "but", for many properties that happen to be
of human interest, such as the absence of buffer-overflow errors, or
the fact that a given program terminates, verification is often fairly
easy to do and specification of the relevant property
is easy. so easy in fact sometimes that it can be automatised. Sriram
Rajamani for example, http://research.microsoft.com/~sriram/ has
recently come up with some surprisingly powerful automatic verification
tools.

in summary, it seems that chaitin is right, but for properties and
programs as simple as those humans care about, formal verification
tends to be possible.

martin

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