Path: utzoo!attcan!uunet!jarthur!usc!ucsd!ucbvax!bloom-beacon!eru!luth!sunic!mcsun!ukc!edcastle!sean
From: sean@castle.ed.ac.uk (S Matthews)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <2870@castle.ed.ac.uk>
Date: 16 Mar 90 10:46:16 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <1423@oravax.UUCP>
Reply-To: sean@castle.ed.ac.uk (S Matthews)
Organization: Edinburgh University Computing Service
Lines: 39

In article <1423@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes:
>In article <2480006@hpcuhc.HP.COM> runyan@hpcuhc.HP.COM (Mark Runyan) writes:
>-As an alternative, someone could post a non-trivial program and ask the
>-program provers to prove it either correct or incorrect...
>
>I like this idea.  Any takers?
>-- 
>------
>Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Ian should know a *lot* better than this, and severely damages his own
credibility by saying it. 

If he were to look in (and he certainly should have already) `Software
development: a rigourous approach (Prentice Hall International, 1980)'
which is one of the oldest books on practical programming development
using formal methods (VDM), he would finnd that the author (Cliff Jones)
describes how he sailed into the the IBM Vienna labs raving about this
wonderful new development technique he had.  The first response was
exactly what we have seen in this news group, followed by an offer by
Jones to verify an implimentation of Early's Parser.  This attempt
failed miserably.  Jones then went on to develop, from scratch, a new
implimentation, and, on comparing that to the original, discovered some
bugs. 

Anyone who expects to be able to do this after Jones (who, if anybody,
knows what he is talking about in formal verification) has admitted that
it is not practical, should expect to be doubted in other statements.

Formal verification is not a snake oil panacea, but some people make it
sound like one and it is no wonder that reasonable people are sceptical
of their claims.

Sean

By the way, if anyone is looking for a convincing example of the
advantages of formal/rigorous development techniques, they could do a
lot worse than check the Development that Jones describes in chapter 18
of that book.