How do we decide if compilation is correct?
Language standards for semantics.
E.g. K Framework
See Finding and Understanding Bugs in C Compilers - property checking for C programs. Proving compilers correct. CompCert, written in Coq Verified Software Toolchain, Vellvm
Conretely how do we capture correctness
P0 in C P1 in asm
Result(P, input) = Rc Rx86 = Result(compile(P), input)
= here refers to semantics
For any program P and any input interpreting P with input in C. is the same as executing compilation of P with input in x86 assembly.
forall P, input: interpret(P, input) = execute(compile(P), input)
italics are assumed correct.