3 ms·
The point is that, by proving the unsafe parts of the standard library correct and Rust's safety guarantees correct, we transitively prove the memory safety (as
by pcwalton 2y ago
The point is that, by proving the unsafe parts of the standard library correct and Rust's safety guarantees correct, we transitively prove the memory safety (as well as data race freedom, etc.) of all safe Rust code (that uses only the standard library). Only proving the unsafe code correct is far less effort than proving all Rust code correct would be. This addresses the common criticism of "what about unsafe code?" when people talk about Rust's safety guarantees. We can use a more powerful system, like Coq, to fill in the gaps that the Rust type system itself isn't powerful enough to handle.
- pron 2y agoSure (assuming Rust's type system were sound, which, I believe, it isn't yet). But my general point -- which isn't at all specific to Rust -- is that with deductive methods, sometimes the effort required may not be worth the added assurance probability they give over unsound methods, while in other cases, deductive methods may be cost-effective. The question of cost-effectiveness is one that always needs to be asked in software assurance. The level of confidence that software requires (as opposed to an abstract algorithm) is not that much higher than one minus the probability of an "unaccounted" failure (such as a hardware failure). Sometimes the extra confidence beyond that point is free, and sometimes it can be very expensive.