qcert icon indicating copy to clipboard operation
qcert copied to clipboard

New route to WASM extraction

Open pkel opened this issue 2 years ago • 0 comments

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

pkel avatar Oct 04 '23 07:10 pkel