how to prove compiler‘s correctness

Formal verification
	Compiler correctness for all input programs
		since the tool to find the proof (theorem prover) is implemented in software and is complex, 
			there is a high probability it will contain errors. 
		One approach has been to use a tool that verifies the proof (a proof checker) which, 
			because it is much simpler than a proof-finder, is less likely to contain errors.
		A prominent example of this approach is CompCert, 
			which is a formally verified optimizing compiler of a large subset of C99.
			
	Translation validation: compiler correctness on a given program
		In contrast to attempting to prove that a compiler is correct for all valid input programs 
			translation validation aims to automatically establish that a given input program is compiled correctly
		compares the intermediate form of the program before and after each compiler pass and verifies the preservation of semantics.
		
Testing
	generates random programs to try to find bugs in a compiler
	minimize a found test case to make it easier to understand