I don't think having to trust the extractor matters much in practice, since you need to trust the compiler for extracted program anyway. Compared to OCaml compi

I don't think having to trust the extractor matters much in practice, since you need to trust the compiler for extracted program anyway. Compared to OCaml compiler, Coq-to-OCaml extractor is simple and small.