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

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

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

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.

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: Sep 30 2023 at 06:01 UTC