Cold water

Konrad Slind <slind@informatik.tu-muenchen.de>

Mail folder: QED
Next message: Zdzislaw Meglicki: "Re: Cold Water"
Previous message: Konrad Slind: "getting a formal education"
In-reply-to: Zdzislaw Meglicki: "Re: Cold water"
Reply: Zdzislaw Meglicki: "Re: Cold Water"

From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: Zdzislaw.Meglicki@arp.anu.edu.au
Cc: qed@mcs.anl.gov
In-reply-to: Zdzislaw Meglicki's message of Fri, 30 Apr 1993 02:00:47 +0200 <wfs6kjOKmlE2M=5GFi@arp>
Subject: Cold water
Message-id: <93Apr30.033243met_dst.8088@sunbroy14.informatik.tu-muenchen.de>
Date: 	Fri, 30 Apr 1993 03:32:33 +0200
Sender: qed-owner
Precedence: bulk


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 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.

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.

Konrad.