Re: Cold water
Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
Message-id: <wfs6kjOKmlE2M=5GFi@arp>
Date: Fri, 30 Apr 1993 10:00:47 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Cold water
Sender: qed-owner
Precedence: bulk
In <8849.9304291129@harris.dcs.ed.ac.uk> dts@dcs.ed.ac.uk writes:
> 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.
There is no reason why such a project should not be established. There
would certainly be enough electronic and software engineers interested
in it and it could certainly get a lot of financing from the industry
too. But this is also the reason why such a project isn't worth fighting
for: it's a free-wheeler - it will become established sooner or later
anyway with everybody's blessing. Mathematics, on the other hand, is a
different game. Most people just put it in the "too hard" basket. A
grand and widely publicised project like QED could greatly help in
getting it out of there and making it a part of every day life. It would
also greatly help in "making computers think". Mathematics in this
respect is more challenging than just software and hardware verification
because its concepts and language are so much richer while still formal
and therefore, at least in principle, amenable to automation. A working
QED system would also be more broadly applicable than software and
hardware verification systems.
Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS,
The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601,
Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158