3 ms·
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
by turbinerneiter 5y ago
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?
- crocal 5y agoFYI, this has been done: https://compcert.org/ https://compcert.org/
- gpm 5y ago> 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).