Theorems that express the correctness of individual optimizations cannot be composed unless they refer to the same intermediate languages and semantics. The correctness of this transformation is conditional upon the absence of certain features from the program being optimized. For example, this transformation would be incorrect if the program terminates by calling a library procedure that reports the number of words that have been allocated for ref values. When proving the correctness of compiler optimizations, we probably wish to pretend that such library procedures do not exist. My point is that any theorem that states the correctness of this optimization must contain hypotheses that rule out the use of such library procedures.
Most optimizations are brittle.
For practical work on compiler correctness, we need general theorems that characterize a class of extensions for which an optimization remains correct. Compilers use intermediate languages to express optimizations that may not even be expressible in the source language. We cannot prove the correctness of a realistic compiler by combining theorems that assert the correctness of individual optimizations with respect to a single source semantics. We make the situation even worse by trying to use a hodgepodge of abstract interpretations over differing non-standard semantics for the source language. We need to direct more attention to intermediate languages, to the subtle changes in their semantics after each phase of optimization, and to the formulation of theorems that apply to a variety of intermediate semantics.