Re: Paper on reflection

John Harrison (John.Harrison@cl.cam.ac.uk)
Thu, 04 May 1995 12:22:18 +0100

| 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.