> 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?
Because Rust is not Verus, and not all unsafe code needs formal-verification-level of rigorousness. Also, there are other verifiers as well.
bcjdjsndon · · focus · HN ↗
Why then does rust even need the unsafe keyword?
afdbcreid · · focus · HN ↗