Lessness (May 09 2021 at 10:27): 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?
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?
Emilio Jesús Gallego Arias (May 09 2021 at 13:29):key info here is "what is written in each language"?
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.
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: Apr 16 2024 at 16:01 UTC