Skip site navigation (1)Skip section navigation (2)
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-chat" 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>