qcert
qcert copied to clipboard
New route to WASM extraction
Webassembly garbage collection is about to be released in the first browsers. This unlocks using the two competing ocaml-to-wasm compiler projects for extraction from Coq via OCaml to Wasm.
https://discuss.ocaml.org/t/an-update-from-the-ocaml-wasm-organization/13114
If Coq to Wasm is too much, another thing worth trying could be to replace the current WASM runtime (Assemblyscript) with an OCaml version.
https://github.com/querycert/qcert/tree/master/runtimes/assemblyscript