Hacker News Reader

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/

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.