3 ms·

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://c

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.