‹ BackHN Continuity

Thread

Developing provably correct Rust code with Verus

164 points · 79 comments · Betelbuddy

  1. bcjdjsndon · · focus · HN ↗
    > 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?

    1. ijustlovemath · · focus · HN ↗
      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
      1. bsaul · · focus · HN ↗
        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.
Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.