Stream: Coq users

Topic: Formally verified javascript?


view this post on Zulip Lessness (May 09 2021 at 10:27):

What should I do/learn/study if I want, for example, to make formally verified GCD function for BigInts?

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2021 at 13:24):

Hi @Lessness , can you provide a few more details, what is exactly what you would like prove?

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2021 at 13:29):

key info here is "what is written in each language"?

view this post on Zulip Lessness (May 09 2021 at 16:21):

In Coq there should be predicate (what does it mean to correctly calculate GCD of two BigInts), and the javascript function defined as mathematical object. Then I prove that the function matches the specification.
In the end one could transform the function into string that's the function "extracted" to javascript (that's optional).

I googled and found about JSCert, that is something to study, I believe.

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2021 at 19:49):

Indeed jsCert is a good start for reading, but in general this kind of setup is still a complex endeavor as Coq verification here tends to be of total correctness, so you need to account for some kind of compilation which the two corresponding semantics.


Last updated: Jan 28 2023 at 07:30 UTC