4 ms·

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 2y ago
  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.html https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.ht... This is used by compcert: https://compcert.org/ https://compcert.org/
  • user2342 2y ago
    Yes, I know, I mentioned the extraction. My question was whether it can help detecting translation errors from the first step.
    • cccbbbaaa 2y ago
      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.