3 ms·
UB in unsafe rust sometimes "leaks" outside the unsafe scope and cause crashing elsewhere. If rust can pair with a proof checker and let user write some correc
by j16sdiz 4y ago
UB in unsafe rust sometimes "leaks" outside the unsafe scope and cause crashing elsewhere.
If rust can pair with a proof checker and let user write some correctness proof, it can be way more useful than the current borrow checker.
- mr_00ff00 4y agoThe correctness proof idea sounds intriguing. Ada does this already yes? And do you have any examples of where UB from unsafe rust leaks to outside the program? Surely you would look back at the unsafe code always to fix it.
- dist1ll 4y agoThere is a huge body of work around proof-based programming. If you're looking for a full blown SMT solver and general purpose dependently-typed PL have a look at F* https://fstar-lang.org https://fstar-lang.org
- satvikpendem 4y agoAre you talking about Miri, or something even stronger?
- Arnavion 4y agoMiri doesn't do proofs. It only checks the test cases that you run under it.
- satvikpendem 4y agoInteresting, I wonder if there are any good proof verifiers for Rust.
- throwawaymaths 4y agoIsn't there already a project for that? Though I think at that point you might as well formally verify zig as a means to get memory safety, resource provenance, and data race safety. The idea that memory safety must be baked into the type system is belief by the existence of provenance tracking macro/crate in rust since that exists specifically to track memory in unsafe; rust is basically 'discovering' a need to inventing what zig will need to invent for memory safety.
- kaba0 4y agoCorrectness proof? That’s like almost impossible, formal verification is just not scalable, insanely complex and it will never be done by your average developer. The only way we can do proofs (on certain things) is restricting code, like non unsafe rust. If it would be feasible, why wouldn’t we just continue to use C and be happy with our verified C codes?