# Re: Root Logics

beeson@cats.UCSC.EDU
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
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?