I dealt with this issue while proving the correctness of GMP square root. This program has been proved at different levels of abstraction. The description of the imperative implementation has been performed using the Correctness tool. It takes into account every detail of the implementation, including checking whether pointer arithmetics and boundaries for modified parts of the memory are correct throughout the execution of the program. The mathematical properties of the algorithm are common to all formal descriptions; they were proved once at the mathematical level and then reused in the functional and imperative descriptions.
I also studied how to reuse formal proofs when shifting from one representation to another of some data. For this, I developed a tool to abstract away the computational properties associated to an inductive datatype. This tool acts as a proof term transformer. It allows us to transform statements and their proofs using a given representation of some data into new correct statements and correct proofs using a new representation for these data. Using this partially-automated technique, I managed to to shift from Peano's representation of numbers to the binary one in the Arithmetic library of Coq.
Below you can find links to some papers or proof developments: