I don't expect the compiler to produce "optimal" code in non-trivial cases, but being able to prove to the compiler that some high level code corresponds to some optimized assembly is high on my wishlist (obligatory list: coq, lean, framac, k-framework, f* and many others)