From owner-qed Fri Oct 28 16:38:15 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id QAA19107 for qed-out; Fri, 28 Oct 1994 16:36:19 -0500
Received: from maui.cs.ucla.edu (Maui.CS.UCLA.EDU [131.179.128.11]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id QAA19099 for ; Fri, 28 Oct 1994 16:36:10 -0500
From: chou@cs.ucla.edu
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu
(Sendmail 4.1/3.26) id AA18560;
Fri, 28 Oct 94 14:36:03 PDT
Message-Id: <9410282136.AA18560@maui.cs.ucla.edu>
To: qed@mcs.anl.gov
Subject: Who are the intended customers of QED?
Date: Fri, 28 Oct 94 14:35:50 PDT
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
One thing about QED that I never quite understood is:
Who are the intended customers of QED?
The recent discussion seems to assume that mathematicians are
the intended customers. For instance, David McAllester wrote:
> Mathematicians are concerned with truth. From a marketing perspective
> it seems better to speak their language.
But are mathematicians really interested in something like QED? I am
not a mathematician, so I don't really know. But my impression is that
most mathematicians (logicians included!) are quite happy with informal
proofs and the social process of debugging such proofs. Furthermore,
it seems to me safe to assume that unless using a mechanical theorem
prover can be as easy as writing informal proofs, most mathematicians
will NOT be interested in something like QED. Unfortunately, as anyone
who has used a mechanical theorem prover knows, we don't have such
technologies yet. Is building such easy-to-use theorem provers a main
goal of QED?
Moreover, even if most mathematicians are interested in something like
QED, are they (collectively) willing and able to pay for it? I personally
don't think so, but again, I don't know as I am not a mathematician.
Shouldn't the QED community pay more attention to other potential
customers? Especially those who can PAY for it?
Cheers,
Ching-Tsun Chou