- Use the assembly code I give you (or some other forfm - RTL, transformed C code, etc.)
- But you, Mr. Compiler, should do a formal equivalence proof
- using various command line switches
- heck, I can even sketch the steps of the proof. But I want you, the compiler, to chedck it.
Reason: oftentimes I optimize code by
- Looking at compiler output
- Handwriting assembly
- Then trying to figure out compiler switches to cause the compiler to GENERATE this code.
Seems wasteful, since I already know the code that I want the compiler to generate.
It is often easier to verify equivalence of unoptimized and optimized form than it is to generate the optimized form. Similarly, it is often easier to check a proof than it is to generate a proof.
Moreover, if you can specify code generation for just a small subset, then you can let the compiler do what it does well: the bookkeeping to connect that small subset to the rest of the world.
