Suppose I want to solve Project Euler exercise #1 in javascript and verify the program... Is it possible today?

I used to do a lot of internet searches to find out. I guess the answer is possible, but very hard. Correct me if I'm wrong. I can only say with confidence that there's a lot of stuff that's missing in the ecosystem, and if we want something, we have to work hard and contribute to the community.

Lessness said:

Suppose I want to solve Project Euler exercise #1 in javascript and verify the program... Is it possible today?

You could write the program in WhyML, verify it using Why3 and Coq, and finally extract it to OCaml/Javascript. And guess what, someone already did so: https://toccata.gitlabpages.inria.fr/toccata/gallery/euler001.en.html

Yeah, that's definitely an option. I could also write the program in Coq directly and extract to OCaml, then transpile OCaml to JavaScript. Writing straight JavaScript and verifying it in Coq, however, is much harder. (disclaimer: not a researcher, I can be wrong)

If you directly want to verify Javascript code, you can use Jscert. It is not really harder than the other approaches. It is just a lot more tedious because there is absolutely no documentation nor examples.

we have one project in Coq-community which uses js_of_ocaml to get "verified" JavaScript code: https://github.com/coq-community/sudoku

The most maintained JavaScript related Coq definitions are likely in https://github.com/querycert/qcert

@Guillaume Melquiond since you are the maintainer of the why3-coq opam package. Do you know whether the Coq backend for why3 still works? (Is there any documentation available?)

Yes, it is routinely used. There is some light documentation at https://why3.gitlabpages.inria.fr/why3/itp.html

Last updated: Dec 01 2023 at 06:01 UTC