> 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 i

> 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