> Not at all. Rust's safety guarantees work in practice. They don't just work in practice. I spent 3 months last semester being taught in the separation logic

> Not at all. Rust's safety guarantees work in practice. They don't just work in practice. I spent 3 months last semester being taught in the separation logic "Iris", which is used to formally prove the safety guarantees of Rust as part of the RustBelt[0] project. That was under Lars Birkedal, for anyone curious. Rust is a language I love doing actual work in, but it's also one I really like from the perspective of the theoretical backing. [0] : https://plv.mpi-sws.org/rustbelt/