[user2342]

Yes, I know, I mentioned the extraction.

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

[cccbbbaaa]

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.