Date: 15 May 1999 12:34:45 +0200 From: Dag-Erling Smorgrav <des@flood.ping.uio.no> To: chat@FreeBSD.ORG Cc: Wes Peters <wes@softweyr.com>, hackers@FreeBSD.ORG Subject: Re: BSD, GPL, the world today. Message-ID: <xzpiu9u39kq.fsf@localhost.ping.uio.no> In-Reply-To: Nik Clayton's message of "Sat, 15 May 1999 01:48:23 %2B0100" References: <199905131530.LAA04222@etinc.com> <xlxso8z2w76.fsf@gold.cis.ohio-state.edu> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org>
next in thread | previous in thread | raw e-mail | index | archive | help
Nik Clayton <nik@nothing-going-on.demon.co.uk> writes: > Didn't Knuth say "I've only proven TeX to be correct, I haven't tested > it" or some such? TeX is far too large to undergo even a partial correctness proof, much less a total correctness proof (I'm not even sure total correctness can be proven; cf. the halting problem). I seriously doubt Knuth ever considered undertaking such a task. It's quite possible, though, that he's proven partial or total correctness of some portions of it (such as frequently-used low-level routines). Correctness proofs are very time-consuming, because they can't be automated. There are experimental tools which can assist with part of the work (e.g. the partially-completed Abel project at the University of Oslo: <URL:http://www.ifi.uio.no/~prover/abel/>) but the hardest part of the job - finding loop and type invariants and post- and pre-conditions which the prover can use as starting points - must still be done manually. The day when a computer can prove partial correctness of a program on its own is the day when computers gain the ability to program and debug themselves - and we'll all be out of a job and out of a hobby. > I could well be mis-remembering a quote about some other app. As I remember it, the quote referred to a noddy program used as an example in a paper or lecture. Knuth had proven the program to be correct, but had never actually compiled it. DES -- Dag-Erling Smorgrav - des@flood.ping.uio.no To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-hackers" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?xzpiu9u39kq.fsf>