3 ms·
The size of programs (as opposed to libraries, which could be easier because their code is not nearly as self-interacting) that has been end-to-end verified wit
by pron 2y ago
The size of programs (as opposed to libraries, which could be easier because their code is not nearly as self-interacting) that has been end-to-end verified with semi-automated deductive proof systems like Coq is quite small. In fact, the size of programs that can be verified in this way has grown at a slower pace than the growth in the average size of programs overall. While sound software verification (i.e. a 100% conformance to a spec) certainly has its place (usually to prove the correctness of some core algorithms), it doesn't scale well, which is why there's been a shift in research into unsound methods because the cost of 100% assurance can be 10x that of 99.9999% assurance, and the difference in probability may fall below that of non-software failures (after all, a physical system cannot be proven to conform to a spec) or the probability of a spec that doesn't conform well enough to reality.
- pcwalton 2y agoThe 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.