From lusk Sun May 15 17:38:09 1994 Received: from uqcspe.cs.uq.oz.au (uqcspe.cs.uq.oz.au [130.102.192.8]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id RAA26338 for ; Sun, 15 May 1994 17:35:16 -0500 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; Mon, 16 May 94 08:34:43 +1000 Received: by everest (5.0/SMI-SVR4) id AA14447; Mon, 16 May 1994 08:34:41 --1000 Date: Mon, 16 May 1994 08:34:40 +1000 (EST) From: John Staples Subject: Has it all been said? To: qed@antares.mcs.anl.gov Cc: staples@cs.uq.oz.au Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Length: 2448 Subject: Has it all been said? ============================== Good to see there's life in the QED discussion as the workshop approaches. However I'd like to see more of a sense of urgency: the sort of attitude that develops in a project when one realises that, unless we settle down to making decisions the whole thing is going to be a disaster! I don't mean we should rush through the basic strategic issues, to get down to detail. Indeed I think the whole concept needs reviewing, partly to reestablish commitment, partly to consider how/whether to respond to the various concerns that have been raised. The vital thing at this stage is to have a strategic plan that will attract support - from all those whose support we need, intellectual and otherwise. As I see it, a key problem with the current style of discussion is that a vision of an ideal future - computer representation of all mathematical knowledge is not being distinguished from a project proposal. A project proposal can be inspired by such a vision, but needs to go on to set priorities and intermediate goals. It should also address significance - what good would it do to achieve the project goals? From my perspective it's clear that there's potentially a huge payoff in increased trustworthiness of critical computer systems, since QED has the potential to greatly increase the productivity of developing formally verified computer systems. One more point. I strongly suspect that peer review at this time of any QED-like project proposal *by mathematicians* would be negative, or negative enough to miss out on funding. There are too few mathematicians who have any idea of what benefits could be obtained, and too many who heartily despise formality (I speak as a mathematician!). Mathematical peer review is to be expected if the project proposal simply identifies the goal as mathematical. I suggest we need to broaden the peer base, by bringing out the value of assisting professionals who need mathematics but aren't mathematicians - i.e. assist them to access mathematical knowledge, and to make large but rather routine increments to it. It probably wouldn't hurt to mention that, though the access of nonmathematicians to mathematics would be greatly increased, this would in turn increase the demand for mathematics and for mathematicians. I'll be out of email contact for several days from now, and look forward to the workshop. John Staples