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