Hacker News Reader

Comment by kartD | Hacker News Reader

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.

View on HN

> 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

There is a PR for a Lean backend producing both C++ and Rust: 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.

My 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.

I actually started the project in Isabelle: 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.

All of these look really interesting, I'll take a look at time. Thanks everyone!

Reply on news.ycombinator.com