[bennofs]

Yes, that is a limitation. But this limitation is not too bad.

In many cases, a bug in the translation simply makes the proof impossible. Somebody then investigates why the proof does not go through and finds the bug in the translation.

We only have a problem if the bug in the translation specificially cancels a bug in the original code. If there is no systematic risk, it is quite unlikely that two bugs cancel each other in this way.

[im3w1l]

Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier happily asserts that the translated program does not cause use after free.

I doubt the translation would be that bad but it could have more subtle issues of the same kind.

[bennofs]

My argument is that you typically also check other properties, like properties describing what your program should do. These other properties likely wouldn't be satisfied by a nop program, and hopefully the same is true for many subtle issues.

[user2342]

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?

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