Daniel Bernstein has given an interesting talk about "the death of optimizing compilers" (PDF slides at https://cr.yp.to/talks/2015.04.16/slides-djb-20150416-a4.pdf) claiming that less and less of our code is in that middle ground where it's performance-critical enough to risk running it through an optimizer but not so performance-critical that it needs to be rewritten in assembly.

If we think of the high-level source code (whether in SQL, JS, or Python) as being a functional spec that the low-level implementation should provably follow, maybe we should check them both in, and at build time, run a proof assistant to verify that the implementation still complies with the spec? Rather than running an optimizing compiler every time. I think this is what nanolith is suggesting in https://news.ycombinator.com/item?id=41965701.

Maybe you run the optimizing compiler once when you first write the code, and again when the proof assistant tells you an optimization is no longer valid, but you check the output before you check it in. Or maybe you have the compiler running all the time on a GPU cluster looking for new optimizations.