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"?
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