> Do you then transiently get all the achievements of all safety critical software that was then programmed with it? It's possible to write incorrect code and

> Do you then transiently get all the achievements of all safety critical software that was then programmed with it? It's possible to write incorrect code and compile it with a correct compiler, so I don't think so. It's more like a citation that proven correct programs can use to say "I wrote this program correctly (see my own proof), and I compiled it correctly (see citation), thus I have a correct executable file". > I guess the Rust memory safety guarantees are based on some proofs? People have retroactively come up with formal proofs for much of it, but I believe the initial design was just based on intuition not a proof. For unsafe code some of the exact details of the memory model are still being worked out too (and thus definitely aren't proven correct).