| >Note that none of those code extractors are verified to be >correct themselves, lacking a formalization of the target >language's semantics. CertiCoq project aims to provide a certified compiler from Coq into CLight (formalized subset of "Safe C"). In this respect, it is superior to what you have mentioned, I guess. Offtopic: Lean's effort seems strange to me. Usage of C++
as its implementation language gets me really nervous, I feel doubt in its reliability. |
Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways:
1. The tool crashes a lot
This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++.
2. You don't feel safe trusting it when it says it proves something
Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of universes, and there exist independent typecheckers written in Haskell <https://github.com/leanprover/tc> and Scala <https://github.com/gebner/trepplein>. I have an in-progress one written in Rust as well.
Meanwhile, Lean is quite fast, the metaprogramming is lovely, and there are some really awesome tools in the pipeline.