Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id MAA09338 for qed-out; Mon, 1 May 1995 12:43:08 -0500
Received: from pnl.gov (gate.pnl.gov [130.20.64.36]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id MAA09326 for <qed@mcs.anl.gov>; Mon, 1 May 1995 12:42:56 -0500
From: rv_harris@ccmail.pnl.gov
Registered-mail-reply-requested-by: rv_harris@ccmail.pnl.gov
Received: from ccmail.pnl.gov by pnl.gov (PMDF V4.3-13 #6012)
 id <01HPZI7D0TC000004Y@pnl.gov>; Mon, 01 May 1995 10:43:16 -0700 (PDT)
Date: Mon, 01 May 1995 10:31 -0700 (PDT)
Subject: Re: Paper on reflection
To: pollack@cs.chalmers.se, dam@ai.mit.edu, ma_friesel@ccmail.pnl.gov
Cc: qed@mcs.anl.gov
Message-id: <01HPZI7DCEKM00004Y@pnl.gov>
MIME-version: 1.0
Content-transfer-encoding: 7BIT
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799352364.003

>Subject: Paper on reflection
>Author:  dam@ai.mit.edu
>Date:    4/30/95  11:44 AM
>... Of course to use a C
>program in a foundational verifier one would have to verify C (as John
>notes). 
>  ...      David

Not to mention having to verify the operation of the hardware on which the C 
code is running (as per the recent Pentium flap).

Rob Harris