Nik Clayton <n...@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 - d...@flood.ping.uio.no To Unsubscribe: send mail to majord...@freebsd.org with "unsubscribe freebsd-hackers" in the body of the message
