Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 30 Apr 1993 03:57:58 +0100
Received: by antares.mcs.anl.gov id AA27779 (5.65c/IDA-1.4.4 for qed-outgoing);
          Thu, 29 Apr 1993 21:56:20 -0500
Received: from tuminfo2.informatik.tu-muenchen.de by antares.mcs.anl.gov 
          with SMTP id AA27771 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Thu, 29 Apr 1993 21:56:16 -0500
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57668>;
          Fri, 30 Apr 1993 04:56:02 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8088>;
          Fri, 30 Apr 1993 04:55:35 +0200
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 04:23:36 +0200 <4fs8qcKKmlE20=5L0r@arp>
Subject: Cold Water
Message-Id: <93Apr30.045535met_dst.8088@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 30 Apr 1993 04:55:20 +0200
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


Zdzislaw Meglicki gives some examples of advanced mathematics and says
that verification systems might never draw on this knowledge. I agree. I
guess I should make it clear that I am an advocate of doing verification
in a system of logic adequate for the formalization of mathematics.
Trying to get away with a simpler system may be unwise in the long run,
since who knows what models may become important in the future for
verification?

Konrad.