Delivery-Date: 
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: qed@mcs.anl.gov
Subject: Cold water
Message-Id: <93Apr23.030459met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 23 Apr 1993 03:04:55 +0200
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


As someone who has been impressed by the progress in the verification of
hardware and software over the past few years, I think that QED (as
manifesto'ed) is a path best untaken. Specifications of computer systems
often draw very little from conventional mathematical knowledge of the
sort that QED is aimed at codifying. Formalized conventional mathematics
is a source to draw from, not a goal. How reasonable is a massive
project that

    a) may or may not serve the needs of mathematicians, who so far seem
       immune to the attractions of actual formalized proofs and 

    b) will distract from, if not impede (by diversion of talent),
       progress in verification, which is demonstrably of use to
       computer manufacturers and software writers?

To phrase things bluntly, which group - mathematicians or computer
companies - have more money? And what are their needs?

Having divested myself of these opinions, I would like to note that I
would dearly love to have some sort of "community bin" of math and
computer theories. I just think that it should be a byproduct, not a
holy grail.

Konrad.