3 ms·
Write the code and proofs in Coq. Coq can output OCaML. I believe OCaML can compile to JavaScript. That will allow you to verify the pure functions. It
by mdnahas 3y ago
Write the code and proofs in Coq. Coq can output OCaML. I believe OCaML can compile to JavaScript.
That will allow you to verify the pure functions. It will not verify the input/output that will also be necessary.