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 ; 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