The problem that you are describing occurs when you are trying to optimize a piece of idiomatic functional code that you have already written. Perhaps the solut

The problem that you are describing occurs when you are trying to optimize a piece of idiomatic functional code that you have already written. Perhaps the solution could be to keep the code you have already written, and write a low-level, highly-optimized replacement alongside it, then have the compiler verify that the low-level code is provably identical in its output to the original function. If the code passes this test, then it is replaced with the optimized version. If you change either piece of code, and they do not match each other, then your code will not compile.