I've done this. In my experience it ends up stuck in local minima from which there are no obvious correctness-preserving improvements. Add Monte Carlo to esca

I've done this. In my experience it ends up stuck in local minima from which there are no obvious correctness-preserving improvements. Add Monte Carlo to escape valleys and this mode of exploration is still too timid to find anything close to optimal. When you find a truly optimal solution, you end up with the least satisfying proof of correctness: "Here's this this inscrutable formula; I verified that it produces the right output for all possible inputs."