Path: utzoo!attcan!uunet!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.theory
Subject: Re: Proof theory (was Re: Academic legend)
Message-ID: <1321@oravax.UUCP>
Date: 6 Feb 90 14:55:43 GMT
References: <20433@watdragon.waterloo.edu> <2072@rex.cs.tulane.edu> <20010@netnews.upenn.edu> <1319@oravax.UUCP>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 18

In article <1319@oravax.UUCP> harper@oravax.UUCP (Douglas Harper) writes:
-In article <20010@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes:
-- PS: Still waiting for the formal spec and verification of the
--  triangle program.-a.
-
-He will have it, but it will take some time to build the theory up from
-the axioms.  The verification in terms of a specification governed by
-that theory is already completed.  I intend to post the final version
-in sci.logic.  If enough people request it in the meantime, I'll
-cross-post it here when it's done.

I request that you ONLY post it in comp.theory.  It seems to me that
proofs of correctness of programs are not really that interesting from
the point of view of mathematical logic.
-- 
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur