Delivery-Date: 
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@mcs.anl.gov
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