What if you proof the correctness of a compiler? Do you then transiently get all the achievements of all safety critical software that was then programmed with it?
The value of the proof comes from the things it enables. I guess the Rust memory safety guarantees are based on some proofs?
> 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).
The value of the proof comes from the things it enables. I guess the Rust memory safety guarantees are based on some proofs?