Comment by 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/