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.