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.
wme@dweazel.sw.mcc.com (Michael Evangelist) (07/13/90)
> 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 ...). This is only one of the beeves and not the most important. What if computers had been available for case checking a hundred years ago and had been used to establish the four-color conjecture as a mathematical fact? Much graph theory would never have seen the light of day. Are any mathematicians still working on a theory adequate to establish the conjecture by traditional methods?
jha@lfcs.ed.ac.uk (Jamie Andrews) (07/16/90)
In article <3964@dweazel.sw.mcc.com> wme@dweazel.sw.mcc.com (Michael Evangelist) writes: >This is only one of the beeves and not the most important. What if >computers had been available for case checking a hundred years ago >and had been used to establish the four-color conjecture as a >mathematical fact? Much graph theory would never have seen the light >of day. This is a bit silly. If computers had been available, period, a hundred years ago, then the world would be an inconceivably different place, and I doubt that the loss of the graph theory you speak of would be noticed. For one thing, the philosophy and science of program correctness would be about 80 years older, and I'm sure we'd have a lot of very valuable results in that field. Who knows, we may even have transcended the silly bickering that characterizes it today. --Jamie. Original material copyright (c) 1990 by Jamie Andrews; jha@lfcs.ed.ac.uk for distribution only on unmoderated USENET newsgroups. "If you try to leave this room, I'll tackle you." -- Don Getty to Clyde Wells