It is a common situation when one has two implementations of the same function, one being straightforward but slow, and the other being fast but complex. It would be nice to be able to check if these two versions are equal to catch bugs in the more complex implementation.
This common situation is often actually one of the harder ones to prove, I say coming from proving a few of them in Coq. The thing is that a lot of the common optimizations (e.g., TCO) completely wreck the inductive structure of the function which, in turn, makes it difficult to say interesting things about them.[1]
The traditional approach is to derive the efficient version from the simple, obviously correct version, by a series of small code transformations. The steps would include meaning-preserving equivalences as well as refinements (where implementation decisions come in to narrow down the set of equivalent code). Advantages: codes are equivalent by construction (modulo implementation decisions), and the relationship is documented (so you can replay it in case requirements changes make you want to revisit some implementation decisions). Even with modern provers/assistants, this should be easier than trying to relate two separately developed pieces of code, though I can't speak from experience on this last point. But there have been derivations of tail-recursive code from the general form (don't have any reference at hand right now). Claus