Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 29 Apr 1993 13:31:16 +0100 Received: by antares.mcs.anl.gov id AA11142 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 29 Apr 1993 06:31:11 -0500 Received: from dcs.ed.ac.uk (stroma.dcs.ed.ac.uk) by antares.mcs.anl.gov with SMTP id AA11134 (5.65c/IDA-1.4.4 for ); Thu, 29 Apr 1993 06:31:01 -0500 Received: from harris.dcs.ed.ac.uk by dcs.ed.ac.uk id aa07431; 29 Apr 93 12:29 BST 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@mcs.anl.gov 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