3 ms·

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees Why then doe

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees Why then does rust even need the unsafe keyword?

ijustlovemath 17d ago
I'd rather have all the unsafe code scoped and the safety invariants explained than the alternative. You still can't do a whole class of scary things in an unsafe block; common misconception
- bsaul 17d ago
  That's indeed a weird feeling when going back to another language after having coded in rust. First you're happy not having to write any "unsafe" keyword. Then you're horrified for the very same reason.
- bcjdjsndon 17d ago
  Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it, and hence, why do we even need unsafe if the compiler can do it.
  - Jtsummers 17d ago
    > 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.
  - ijustlovemath 17d ago
    It generates additional code that's fed into an SMT solver. Poor compiler performance is a top issue developers have with Rust, which they're working to solve. I think adding this layer into every piece of code (which is probably impossible since inferring the invariants is essentially inferring your business logic) would eat away gains they've achieved. I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
hwayne 17d ago
There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.
afdbcreid 17d ago
Because Rust is not Verus, and not all unsafe code needs formal-verification-level of rigorousness. Also, there are other verifiers as well.

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees Why then does rust even need the unsafe keyword?

ijustlovemath 17d ago

I'd rather have all the unsafe code scoped and the safety invariants explained than the alternative. You still can't do a whole class of scary things in an unsafe block; common misconception

bsaul 17d ago
That's indeed a weird feeling when going back to another language after having coded in rust. First you're happy not having to write any "unsafe" keyword. Then you're horrified for the very same reason.
bcjdjsndon 17d ago
Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it, and hence, why do we even need unsafe if the compiler can do it.
- Jtsummers 17d ago
  > 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.
- ijustlovemath 17d ago
  It generates additional code that's fed into an SMT solver. Poor compiler performance is a top issue developers have with Rust, which they're working to solve. I think adding this layer into every piece of code (which is probably impossible since inferring the invariants is essentially inferring your business logic) would eat away gains they've achieved. I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.

hwayne 17d ago

There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.

afdbcreid 17d ago

Because Rust is not Verus, and not all unsafe code needs formal-verification-level of rigorousness. Also, there are other verifiers as well.