Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id GAA13303 for qed-out; Thu, 4 May 1995 06:34:12 -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 GAA13293 for ; Thu, 4 May 1995 06:34:03 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 4 May 1995 12:22:53 +0100 To: qed@mcs.anl.gov Subject: Re: Paper on reflection In-reply-to: Your message of "Wed, 03 May 1995 17:05:43 EDT." <9505032105.AA23164@spock> Date: Thu, 04 May 1995 12:22:18 +0100 From: John Harrison Message-ID: <"swan.cl.cam.:208250:950504112331"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk X-UIDL: 799596352.006 | Even if we used ML for extensions, the correctness of an extension still | assumes correctness of the hardware on which we are ultimately running. Of course, there is a dependence on the correctness of the implementation language compiler and underlying hardware regardless of whether one is interested in reflection. The point is that computational reflection usually involves absorbing the computer implementation of the logic into the logic's abstract description. By contrast, in an LCF system, whatever the merits of the implementation, one can give a simple, coherent account of what the logic is. For a QED-like effort this seems important. John.