A shot in the dark: it could perhaps help in automatically optimizing algorithms by proving that the optimized version is equal to an easily written and reasoned about.
I think reasoning about correctness is easier than about optimizations. Even if you account for a simple complexity model (real computers are a lot more complex, because of techniques like branch prediction or memory caching), proving an implementation as optimal is very hard!
It's often really hard to know if an optimization is "correct"- is the same function as the original, unoptimized version. Formal methods helps here by showing they're equivalent, so you can focus on finding good optimizations instead!