Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 17 May 1995 11:34:15 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA234705232; Wed, 17 May 1995 04:07:12 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA234675222; Wed, 17 May 1995 04:07:02 -0600 Received: from albatross.cl.cam.ac.uk (user sk (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 17 May 1995 11:04:27 +0100 To: heckman@cs.ucdavis.edu (Mark R. Heckman) Cc: homeier@cs.ucla.edu, info-hol@leopard.cs.byu.edu, Sara.Kalvala@cl.cam.ac.uk Subject: Re: Question on Dijkstra Quote In-Reply-To: Your message of "Tue, 16 May 1995 17:57:25 PDT." <9505170057.AA12766@shangrila.cs.ucdavis.edu> Date: Wed, 17 May 1995 11:04:24 +0100 From: Sara Kalvala Message-Id: <"swan.cl.cam.:161640:950517100430"@cl.cam.ac.uk> > In a similar vein, I once read a second-hand quote attributed to > Knuth that said "Beware of bugs in the above code. I have only > proven it correct; I haven't tried it yet." Can anyone help me > find the source of this quote? I am pretty sure it's from: @InCollection{kn:simple_program, author = "Donald Knuth", title = "A Simple Program Whose Proof Isn't", booktitle = "Beauty is our Business", publisher = "Springer-Verlag", year = "1990", editor = "{W.H.J.} Feijen and others" } But I don't have the book at hand to check it. (Mark: the book is available at the library at UCD.) Knuth discusses a subroutine (for conversion between decimal and binary fractions) which could be proved correct by exhaustive simulation (i.e. testing on all inputs), a method which he finds unsatisfactory. He prefers a proof which is ``comprehensible and educational'', a proof that reflects the development of the program. The proof he finally elaborates does indeed lead to some more general ideas. - Sara