The post discusses the translation of Rust's core and alloc crates using coq-of-rust, a tool to translate Rust code to the formal proof system Coq. It describes the challenges faced, the size of the input code, the splitting of generated code, bug fixes, and provides an example. The work is funded by Aleph Zero crypto-currency.
Table of contents
Initial run 🐥 Splitting the generated code 🪓 Fixing some bugs 🐞 Example 🔎 Conclusion 24 Impressions