4 ms·
There is a PR for a Lean backend producing both C++ and Rust: https://github.com/leanprover/lean/pull/1090 https://github.com/leanprover/lean/pull/1090 Note, ho
by derkha 10y ago
There is a PR for a Lean backend producing both C++ and Rust: https://github.com/leanprover/lean/pull/1090 https://github.com/leanprover/lean/pull/1090 Note, however, that this is purely focused on executing Lean code, not integrating with other C++/Rust sources.
- nickpsecurity 10y agoMy first thought was why Lean vs Isabelle/HOL or Coq given all they have that can be leveraged? And selectively depending on how challenging or different you want your project.
- derkha 10y agoI actually started the project in Isabelle: https://github.com/Kha/electrolysis/tree/isabelle/thys https://github.com/Kha/electrolysis/tree/isabelle/thys. Automation was nice, translating Rust traits not so much. You really want them to be type classes, which Isabelle only supports for the single-parametric case. As of right now, the project would probably be easier in Coq. But I'm confident that Lean 3 will eventually feature more powerful automation (and no Ltac). It is, after all, being developed by Leonardo de Moura, one of the creators of Z3.
- kartD 10y agoAll of these look really interesting, I'll take a look at time. Thanks everyone!