> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guaranteesWhy then does rust even need the unsafe keyword?
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.
bcjdjsndon · · focus · HN ↗
Why then does rust even need the unsafe keyword?
hwayne · · focus · HN ↗