Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!cs.utexas.edu!uwm.edu!zaphod.mps.ohio-state.edu!sunybcs!rutgers!netnews.upenn.edu!grad2.cis.upenn.edu!aaron
From: aaron@grad2.cis.upenn.edu (Aaron Watters)
Newsgroups: comp.theory
Subject: Re: Proof theory (was Re: Academic legend)
Message-ID: <20010@netnews.upenn.edu>
Date: 5 Feb 90 20:52:31 GMT
References: <20433@watdragon.waterloo.edu> <2072@rex.cs.tulane.edu> <19983@netnews.upenn.edu> <1318@oravax.UUCP>
Sender: news@netnews.upenn.edu
Reply-To: aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters)
Organization: University of Pennsylvania
Lines: 23

In article <1318@oravax.UUCP> harper@oravax.UUCP (Douglas Harper) writes:
>In article <19983@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes:

>| Proof
>| theories are primarily an abstract object of mathematical discussion
>| and not a used mathematical technique.
>|   -aaron
>
>Mr. Watters is apparently unaware of the widespread use of proof theory
>in pure and applied logic.  
I geuss I am.  I know these people STUDY proof theories -- that's not
the same as using it.  By `use' I did not mean `prove things about.'

>Two applications that readers of this
>newsgroup will immediately recognize are automated theorem proving and
>program verification.

I said `seldom' not `never.'  These uses are hardly widespread
-- especially not by real mathematicians.  
	--aaron

PS: Still waiting for the formal spec and verification of the
 triangle program.-a.