Comment by weinzierl

What I don't quite understand with these efforts is this: If we have to translate the code to Coq manually or semi-manually, isn't the likelihood that we make mistakes there much higher than what we ultimately gain with the formal verification. In other words, how do we know that what we proof is still valid for the original code?