With a powerful type system (think Coq/Lean/...) you can declare the following (for example): forall s:Source, execute_machine_code(compile(s)) = interpret_sou

With a powerful type system (think Coq/Lean/...) you can declare the following (for example): forall s:Source, execute_machine_code(compile(s)) = interpret_source_code(s) And the compiler will only accept your compiler code as being typed correctly if for all possible source code, running the compiled code gives the same result as interpreting the source code directly. In other words, you are proving your compiler to be correct. Think about it as having an infinite number of test cases in a single line. Now that's powerful!