There are a lot of compiler optimizations that uses global analyses/optimizations that are not covered by optimizing a sequence of assembly instructions. Thus,

There are a lot of compiler optimizations that uses global analyses/optimizations that are not covered by optimizing a sequence of assembly instructions. Thus, I doubt that CompCert + STOKE would reach the code quality of production compilers. Nevertheless, I agree that superoptimizers ofter find optimizations that are not considered by the compiler engineers. Another good example is the Optgen tool [1] that also identified missing (machine-independent) optimizations in all production compilers. [1] http://pp.ipd.kit.edu/optgen/ http://pp.ipd.kit.edu/optgen/