> Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it This question only makes sense if you think Verus is part of the Rust

> Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it This question only makes sense if you think Verus is part of the Rust compiler. It's not. And even if it were, the additional annotations are still required to prove that the unsafe block is actually safe. So this could, if integrated into the Rust compiler, help programmers eliminate some unsafe blocks (perhaps even most), but likely not all, and not without additional code proving that the section is safe.