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
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.
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.
bcjdjsndon · · focus · HN ↗
Why then does rust even need the unsafe keyword?
ijustlovemath · · focus · HN ↗
bcjdjsndon · · focus · HN ↗
ijustlovemath · · focus · HN ↗
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.