steve@hubcap.clemson.edu ("Steve" Stevenson) (07/06/90)
Recently, I asked for some comments about proving programs correct. One of the respondants claimed that there had been a long standing bug in the program which only recently had been discovered and corrected. Does anyone have a reference to this or can anyone refute the claim? Thanks -- =============================================================================== Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
blostein@qucis.queensu.ca (Dorothea Blostein) (07/07/90)
Apparently there has been some discussion about the correctness of the programs used to prove the four color theorem. As far as I know, there has not been "a long standing bug in the program which only recently had been discovered and corrected". (As Wolfgang Haken's daughter I certainly would have heard about this from my father.) There have been long-standing rumors of unknown origin about errors in the program. Truly interested parties can refer to Contemporary Mathematics Volume 98, American Mathematical Society, 1989. This 740 page volume is entitled "Every Planar Map is Four Colorable", by Kenneth Appel and Wolfgang Haken. This volume reviews the proof and gives a detailed account of the nature of the errors that have been found, when they were found, how long they took to repair etc. Independent implementations of the necessary algorithms have been used to verify the correctness of the program results. I'll end with a quote from page 22 of the above-mentioned volume: "How does one go about checking a 400-page unavoidability proof for a set of 1476 configurations? J. L. Doob, the most eminent probabilist we know, has stated Doob's Rule: 'If you open a mathematical paper at random, on the pair of pages before you, you will find a mistake.' (A weaker version of Doob's rule replaces the words 'you will find a mistake' by 'there is a mistake'.) ... When the proof was announced in 1976, Doob offered Haken a bet that within five months an error would be found. Haken offered an amended bet that every error that came to his attention would be repaired within two weeks... Haken won that bet, ..."
aaron@grad2.cis.upenn.edu (Aaron Watters) (07/09/90)
Just a comment. The four color proof is often mistakenly cited as a triumphant example of the use of formal methods -- most egregiously in a paper about program derivation by Scherlis and Scott. Just thought I'd point out that the proof is in no sense any more formal than most other proofs you'll find out there, even though it includes an algorithm as part of the proof, together with a claim that the algorithm terminated with a given result. -aaron
valdes+@cs.cmu.edu (Raul Valdes-Perez) (07/09/90)
In article <26843@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes: > ... >Just thought I'd point out that the proof is in no sense any >more formal than most other proofs you'll find out there, I always thought that computer programs were formal objects, and that a computer was a formal system (`formal' doesn't entail `correct'). Isn't that one sense? -- Raul E. Valdes-Perez valdes@cs.cmu.edu School of Computer Science (412) 268-7698 Carnegie Mellon University Pittsburgh, PA 15213
ian@oravax.UUCP (Ian Sutherland) (07/13/90)
In article <4997@milton.u.washington.edu> aesop@milton.u.washington.edu (Jeff Boscole) writes: >Precisely -where- is >the beef with a "proof by an (unverified.by.hand.calculation) computer >program?" I don't understand the meaning of "(unverified.by.hand.calculation)". The beef with a proof by computer program is that computer programs that have not been rigorously checked for correctness are more likely to be in error than proofs written out by human beings (even as prone as the latter are to errors ...). -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur If Janet Bell (formerly of Northwestern) reads this, please get in touch with me.