Re: Cold water

dts@dcs.ed.ac.uk

Mail folder: QED
Next message: guttman@linus.mitre.org: "Re: Cold water "
Previous message: Larry Wos: "reactions"
In-reply-to: Konrad Slind: "Cold water"
Reply: guttman@linus.mitre.org: "Re: Cold water "
Reply: Zdzislaw Meglicki: "Re: Cold water"

From: dts@dcs.ed.ac.uk
Date: Thu, 29 Apr 93 12:29:37 BST
Message-id: <8849.9304291129@harris.dcs.ed.ac.uk>
To: qed@mcs.anl.gov
In-reply-to: Konrad Slind's message of Fri, 23 Apr 1993 03:04:55 +0200 <93Apr23.030459met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Subject: Re: Cold water
Sender: qed-owner
Precedence: bulk

Although the goals of QED seem exciting and worthy, I find myself agreeing
with Konrad Slind to the extent that I believe the potential benefit of
developing a repository of verified software (and/or hardware) components,
together with their proofs, is far more obvious than that of developing
a body of formally checked mathematics.  From a technical point of view,
this also seems to be a more achievable goal.  I don't mean to suggest that
QED is a bad idea; I just wish that the same enthusiasm could be generated
for doing the same thing with software/hardware.

Don Sannella