Stream: Miscellaneous

Topic: Javascript and verified programs?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC