Yes, I know, I mentioned the extraction.

My question was whether it can help detecting translation errors from the first step.

I'm not sure which first step you are talking about. Typically, one would write the program directly in Coq and use the extracted code as-is.