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

Index Home About Blog