First, how is it possible to integrate existing verified code into the QED
approach? In order to answer this question it is necessary to discuss the status
of proofs in QED. My position is that the correctness of QED should guaranteed
by the *communication* of checkable proofs and that only such systems should be
integrated that deliver information which can be extended to full proofs. In
order to integrate the proofs from one system into the QED language, I propose
to employ a constructive meta-logic, in which provably correct transitions from
one formal system into another formal system can be encoded. By this it is
possible to show abstractly that theorems in an existing system can be used in
QED on the one hand, on the other hand the proofs can be constructed concretely
within QED.
Second, I'd like to discuss the question, why QED is needed in mathematics. One
point is that there have been false theorems in mathematics (compare Lakatos'
description of the development of Euler's polyhedron theorem). Another important
point is the striving for correctness at a level as high as possible in
mathematics, a system like QED is the answer of our time to that striving. (Many
good points to this discussion have already been made in this mailing list last
winter.)
Manfred Kerber
+------------------------------------------------------------+
| Manfred Kerber Tel.: (+49)-681-302-4628 |
| Fachbereich Informatik Fax.: (+49)-681-302-4421 |
| B. 36.1, R. 414 e-mail: kerber@cs.uni-sb.de |
| Universitaet des Saarlandes |
| D-66041 Saarbruecken |
| Germany |
| WWW: http://js-sfbsun.cs.uni-sb.de/pub/www/ |
+------------------------------------------------------------+