5 ms·
I actually wanted to know about the reverse operation. Can we get some formal verification and modeling software to generate Rust(or C) code? When I used Uppaa
by kartD 10y ago
I actually wanted to know about the reverse operation. Can we get some formal verification and modeling software to generate Rust(or C) code?
When I used Uppaal in my grad school course, I kept messing up when I tried to hand translating my code from the model.
- seanwilson 10y ago> I actually wanted to know about the reverse operation. Can we get some formal verification and modeling software to generate Rust(or C) code? Haven't tried it but this claims to be able to extract Rust programs from Coq proofs: https://github.com/pirapira/coq2rust https://github.com/pirapira/coq2rust
- derkha 10y agoThere 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!