Hacker News Reader

In case of coq-to-ocaml: is it feasible to do an extraction to OCaml on the translated code and compare it with the original?

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.