[cccbbbaaa]

You can write programs in Coq and extract them in OCaml with the `Extraction' command: https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.ht...

This is used by compcert: https://compcert.org/

[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.