> How do you verify that the machine code actually does what the proof code 
> associated with it asserts?  Doesn't that directly map to the halting problem?

You restrict the generated machine code to that which you can usefully
make proofs about. In practice this turns out not to be so bad.

Remember, the halting problem (and Rice's Theorem) only prevent you
from saying "I can always prove this", not "I can usually prove this".

        - Nathan