A Hoare Logic for Rust · Ticki's blogLately, I've been working on a Hoare-logic-based model of the Rust MIR, which I will introduce in the post. This is a minor step towards a memory model of Rust, and it allows formalization of programs and their behavior. This project was born out of the effort to formalize the Redox kernel and the ralloc memory allocator as well as coming up with a Rust memory model. Here I will walk through the t
