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