[j16sdiz]

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.

[throwawaymaths]

Isn'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]

Correctness 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?

[mr_00ff00]

The 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]

There 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

[satvikpendem]

Are you talking about Miri, or something even stronger?

[Arnavion]

Miri doesn't do proofs. It only checks the test cases that you run under it.

[satvikpendem]

Interesting, I wonder if there are any good proof verifiers for Rust.