Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id EAA01488 for qed-out; Mon, 1 May 1995 04:49:05 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id EAA01483 for <qed@mcs.anl.gov>; Mon, 1 May 1995 04:48:58 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Mon, 1 May 1995 10:48:22 +0100
To: qed@mcs.anl.gov
Subject: Re: Paper on reflection
In-reply-to: Your message of "Sun, 30 Apr 1995 14:44:08 EDT." <9504301844.AA21652@spock>
Date: Mon, 01 May 1995 10:48:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:038010:950501094826"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799333024.001


David McAllester writes:

| It seems to me that cutting-edge black-box theorems will always be
| challenging for a foundational prover unless it can verify and run C code
| or some imperative equivalent.

I think this is true. On the other hand, technological improvements might mean
that we only lag a few years behind the state of the art. Besides, it doesn't,
as David notes, seem very relevant to QED, which is largely concerned with
"textbook" mathematics (and as such is already way behind the state of the
art). In verification applications the problem is more serious, since here
"brute-force" proof techniques are pretty common.

John.