From owner-freebsd-hackers Sat May 15 3:34:56 1999 Delivered-To: freebsd-hackers@freebsd.org Received: from flood.ping.uio.no (flood.ping.uio.no [129.240.78.31]) by hub.freebsd.org (Postfix) with ESMTP id 8325614D58; Sat, 15 May 1999 03:34:47 -0700 (PDT) (envelope-from des@flood.ping.uio.no) Received: (from des@localhost) by flood.ping.uio.no (8.9.3/8.9.1) id MAA48634; Sat, 15 May 1999 12:34:47 +0200 (CEST) (envelope-from des) To: chat@FreeBSD.ORG Cc: Wes Peters , hackers@FreeBSD.ORG Subject: Re: BSD, GPL, the world today. References: <199905131530.LAA04222@etinc.com> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org> From: Dag-Erling Smorgrav Date: 15 May 1999 12:34:45 +0200 In-Reply-To: Nik Clayton's message of "Sat, 15 May 1999 01:48:23 +0100" Message-ID: Lines: 32 X-Mailer: Gnus v5.5/Emacs 19.34 Sender: owner-freebsd-hackers@FreeBSD.ORG Precedence: bulk X-Loop: FreeBSD.ORG Nik Clayton 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: ) 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