Delivery-Date: 
From: beeson@cats.UCSC.EDU
Date: Thu, 22 Apr 93 09:24:20 -0700
Message-Id: <9304221624.AA12041@si.ucsc.edu>
To: qed@mcs.anl.gov, rap@dcs.ed.ac.uk
Subject: Re: Root Logics
Sender: qed-owner@mcs.anl.gov
Precedence: bulk

In order to decide on the organization of QED effort, e.g. on the 
question of whether it is more important to agree on a high-level 
language or a root logic, it will be necessary first to agree on the 
aim(s) of the project, in order to judge the efficacy of various means
in attaining the desired aim(s).

From my point of view, the aim is to provide 
   (1) the means for practicing mathematicians to write machine-checkable 
proofs
   (2)  the means to check those proofs once written
   (3)  the incentive to write such proofs.

I think it is (3) that is most problematic.  People were willing to 
learn TeX, because the reward is immediate.  The incentive to write 
machine-checkable proofs consists, potentially, in two features: 
avoidance of errors, and adherence to a community standard of proof.
The second of these is a long way off.  The first will not be enough 
incentive for practicing mathematicians.   Therefore at first most 
of the authors of such proofs will be graduate students, who have been
asked by their professors or have taken the initiative themselves to 
write machine-checkable proofs of certain theorems.  The proofs they 
will write will be in a high-level language close to mathematical 
practice (unless they are CS grad students whose advisor is directing
a proof-checking research project).  


Do other people have widely differing views of the aim of QED?
Are there mistakes in the above analysis of incentives?