Newsgroups: comp.risks
X-issue: 3.75
From: decvax!utzoo!henry@ucbvax.Berkeley.EDU
Date: Sat, 4 Oct 86 21:12:13 edt
To: ucbvax!CSL.SRI.COM!RISKS@ucbvax
Subject: Mathematical checking of programs (quoting Tony Hoare)

I agree with much of the quoted discussion from Hoare, including the
obvious desirability of rather heavier use of mathematical analysis
of safety-critical programs.  I do have one quibble with some of his
comments, though:

>   ... never even heard of the possibility that you can establish
>   the total correctness of computer programs by the normal mathematical
>   techniques of modelling, calculation and proof. ...
>   A mathematical proof is, technically, a completely reliable method of
>   ensuring the correctness of programs, but this method could never be
>   effective in practice unless it is accompanied by the appropriate attitudes
>   and managerial techniques. ...

I think talk of "total correctness" and "complete reliability" shows excess
enthusiasm rather than realistic appreciation of the situation.  Considering
the number of errors that have been found in the small programs used as
published examples of "proven correctness", wariness is indicated.  Another
cautionary tale is the current debate about the validity of the Rourke/Rego
proof of the Poincare conjecture.  As I understand it -- it's not an area
I know much about -- the proof is long, complex, and sketchy, and nobody
is sure whether or not to believe it.  And this is a case where the specs
for the problem are very simple and obviously "right".  Mathematical proof
has its own feet of clay.  If one defines "effective in practice" to imply
complete confidence in the results, then I would not fly on an airliner
whose flight-control software was written by a team making such claims.
Complete confidence in provably fallible techniques worsens risks rather
than reducing them.

(The apocryphal comment of the aeronautical structure engineer looking
at his competitor's aircraft:  "Fly in it?  I wouldn't even walk under it!")

On the other hand, if one defines "effective in practice" to mean "useful
in finding errors, and valuable in increasing one's confidence of their
absence", I wholeheartedly agree.  One should not throw out the baby with
the bathwater.  If one sets aside the arrogant propaganda of the proof-
of-correctness faction, there is much of value there.  To borrow from the
theme of a PhD thesis here some years ago, proving programs INcorrect is
much easier than proving them correct, and is very useful even if it isn't
the Nirvana of "total correctness".  The mental discipline imposed on program
creation (defining loop invariants, etc.) is also important.

				Henry Spencer @ U of Toronto Zoology
				{allegra,ihnp4,decvax,pyramid}!utzoo!henry