**Mail folder:**QED**Next message:**Konrad Slind: "Cold Water"**Previous message:**Konrad Slind: "Cold water"**Maybe in reply to:**Konrad Slind: "Cold water"**Reply:**Konrad Slind: "Cold Water"

Message-id: <4fs8qcKKmlE20=5L0r@arp> Date: Fri, 30 Apr 1993 12:23:36 +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 <93Apr30.033243met_dst.8088@sunbroy14.informatik.tu-muenchen.de> slind@informatik.tu-muenchen.de writes: > I think Zdzislaw Meglicki has it backwards when he writes > > Mathematics in this respect is more challenging than just software and > > hardware verification because its concepts and language are so much > > richer [...] > Systems like HOL, nuPRL, IMPS, and many others implement logics intended > for the formalization of mathematics. It also happens that they are > successful at doing verification. There's no difference in such systems > between mathematics and verification. What I had in mind is that if you want to verify a circuit or a computer program you may be able to get away with a simpler system (and possibly also a simpler logic) than if you want to talk, say, about symplectic nondegenerate 2-forms on a 2n-dimensional differential manifold. Computer programs and digital circuits at least are discrete systems. I don't know about IMPS, but I am yet to see anyone proving Ahlfors theorem about complex structure of Teichmuller space being Kahler with HOL or nuPRL. When you talk about very elementary mathematics (e.g., basic logic, some elements of number theory, even some elements of set theory) then indeed systems for doing that kind of mathematics and systems for software and hardware verification are very much the same. But if you'd like to move further in mathematics I think that you will need more sophisticated and elaborate systems, whereas you probably won't need that degree of sophistication in verification of discrete systems such as circuits or programs. Hence my remark about a broader area of applicability of QED (if it ever goes in that direction). For example, I could imagine using QED for reasoning about supersymmetries or about renormalisation in Quantum Electrodynamics (also QED!) but many of the facilities of QED that would make that possible probably wouldn't be needed or useful in software and hardware verification (although some might, who knows). 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