Comment by krukah
9 hours ago
Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me
pgrust is incredible btw
Thanks!
I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.
I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.
What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.