Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by nene.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 1 May 1995 18:53:33 +0100
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

>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