3 ms·

I wasn't aware Coq could generate data types for general purpose programming languages. According to the docs, it supports OCaml, Scheme, and Haskell. I think I

• lelf 7y ago
  > Coq could generate data types Not only data types, the code too.
• snaky 7y ago
  Pretty fast C code. > All formal reasoning is done in the Coq proof assistant, and the overall trusted computing base also includes a simple pretty-printer and the C language toolchain. > We further demonstrate that simple partial evaluation is sufficient to transform into the fastest-known C code, breaking the decades-old pattern that the only fast implementations are those whose instruction-level steps were written out by hand. > These techniques were used to build an elliptic-curve library that achieves competitive performance for 80 prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases. As one outcome, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve. Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare. http://adam.chlipala.net/papers/FiatCryptoSP19/ http://adam.chlipala.net/papers/FiatCryptoSP19/
• lelf 7y ago
  > I wish it supported more! C++17 https://github.com/mit-pdos/mcqc https://github.com/mit-pdos/mcqc Scala https://github.com/JBakouny/Scallina https://github.com/JBakouny/Scallina