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.