UP right

What Is the QED Project and Why Is It Important?

My main general reservation about this part of the manifesto is that it doesn't say enough, either to persuade people that the project is worthwhile, or to provide a basis for making the hard choices that have to be made. QED appears to be sustaining an illusion of concensus by avoiding making decisions which will not be acceptable to all.

I have acquired no sense of how decision making works in QED, or even what constitutes membership of this project. Maybe the merits of informality in this area can be argued, but its difficult for me to understand how the project can work if there is no discussion of the topic at all (probably there has been, but its not visible in the manifesto).

Specifically, it doesn't actually say what QED is and it doesn't distinguish between objectives of QED and reasons why QED is a good thing (e.g. benefits which flow from achievement of the objectives)..

UP I can't see why developing QED would need deep mathematical minds. It would be nice if QED turned out good enough that they used it, but developing QED itself shouldn't require much new mathematics (if any).

In the interest of enlisting a wide community of collaborators and supporters, we now mention five reasons that the QED project should be undertaken.
first to help mathematicians cope with the explosion in mathematical knowledge
second to help development of highly complex IT systems by facilitating the use of formal techniques
third to help in mathematical education
fourth to provide a cultural monument to "the fundamental reality of truth"
fifth to help preserve mathematics from corruption

UP first
Its not obvious to me why a proof tool is needed for this purpose.

UP second
Proof tools which are better at doing real mathematics will certainly make formal verification of IT systems easier than it now is. However, the suggestion that formal methods will help us to deal with the growth in complexity of IT systems is doubtful (though frequently made). The formal verification of an IT system is an enterprise which is massively more complex than its development by informal methods, and consequently only relatively simple systems have ever been verified. Moreover, the growth in complexity of both software and hardware is far outstripping any growth in our ability to verify these systems. There is little reason to believe that QED (or any other project) can make much difference to this.

UP third
I happen to believe in the educational value of proof tools, but its not an easy case to make convincingly. Unfortunately the things proof tools can help best with don't occupy much space in the curriculum (e.g. logic!).

UP fourth
"Cultural" reasons may be better at presuading people to participate than they are at persuading people to pay. Does this kind of argument help a grant application to succeed?

UP fifth
I would have thought that most mathematicians would find this line of argument patronising. Those mathematicians most likely to debase the currency by accepting lax standards of rigour are least likely be influenced by the availability of proof tools. If the foundation of mathematics on set theory is the icon to be secured by QED then there is a fifth column already stealing away with it.

right UP HOME RBJ created 5/1/96 modified 16/1/96 c