Let's say you want to prove a compiler correct. How do you express that as a thing you want to prove mathematically? Here us a possible way to do it:

BehaviourMC(compile(src)) = BehaviourE(src)

You are basically saying that the machine code behaviour of the compiled source should be identical to emulating the source directly.

You then need to define what you mean mathematically by machine code etc. until the goal is fully specified.

And then you prove it correct.