Lessness (Oct 24 2022 at 22:11): Lessness (Oct 24 2022 at 22:11):Suppose I want to solve Project Euler exercise #1 in javascript and verify the program... Is it possible today?
Huỳnh Trần Khanh (Oct 25 2022 at 02:49):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.
Guillaume Melquiond (Oct 25 2022 at 03:11):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
Huỳnh Trần Khanh (Oct 25 2022 at 05:39):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)
Guillaume Melquiond (Oct 25 2022 at 06:22):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.
Karl Palmskog (Oct 25 2022 at 06:25):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
Bas Spitters (Nov 22 2022 at 14:32):@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?)
Guillaume Melquiond (Nov 22 2022 at 16:01):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