From owner-qed Mon Oct 31 08:08:54 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id IAA11198 for qed-out; Mon, 31 Oct 1994 08:03:33 -0600
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id IAA11192 for <qed@mcs.anl.gov>; Mon, 31 Oct 1994 08:03:25 -0600
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA15583; Mon, 31 Oct 94 09:03:19 EST
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA13576; Mon, 31 Oct 94 09:03:17 EST
Date: Mon, 31 Oct 94 09:03:17 EST
Message-Id: <9410311403.AA13576@spock>
To: chou@cs.ucla.edu
Cc: qed@mcs.anl.gov
In-Reply-To: chou@cs.ucla.edu's message of Fri, 28 Oct 94 14:35:50 PDT <9410282136.AA18560@maui.cs.ucla.edu>
Subject: Who are the intended customers of QED?
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


   But are mathematicians really interested in something like QED?  ...
   Most mathematicians (logicians included!) are quite happy with
   informal proofs and the social process of debugging such proofs.  ...
   Unless using a mechanical theorem prover can be as easy as writing
   informal proofs, most mathematicians will NOT be interested in
   something like QED.

I agree.  It seems to me that making formal systems easier to use
should be the main objective in verification research, if not QED.  In
my experience the formalization of mathematics is not difficult.  It
is the lack of automated reasoning power that makes verification
systems hard to use.  Things that are obvious to people are just not
obvious to the machine and people hate having to prove extremely
obvious statements.

I don't know of any papers published by system designers where an
important theorem about an inference mechanism, like a completeness
theorem, has been machine verified before publication.  If we, the
most expert users, don't use them in our own mathematics how can we
expect other less formally oriented mathematicians to use them?  I
think we have a long way to go.

   Shouldn't the QED community pay more attention to other potential
   customers?  Especially those who can PAY for it?

The main source of economic support seems to come from applications to
hardware and software verification.  I suspect that the impediments to
practical verification in engineering are very similar to the
impediments to practical verification in mathematics.


	David