> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code
what about proving safety of not-unsafe code? The meme that rust is "safe" is becoming tiring. Does this thing allow proving absence of infinite loops? Bounded resource use? Correctness of comparison operations? Etc.
Also, why is there still no hardware tagging to simply prevent memory misuse at cpu level, if it actually is such an important issue?
Objection was against "memory safety" somehow having become "safety". Here is an epic tool that allows one to attach and formally prove assertions. Genuinely impressive and massively useful.
Yet the pitch is that it is needed for the "unsafe" unsafe code, to make it "safe". Not for all code, to make all code safe.
112233 · · focus · HN ↗
what about proving safety of not-unsafe code? The meme that rust is "safe" is becoming tiring. Does this thing allow proving absence of infinite loops? Bounded resource use? Correctness of comparison operations? Etc.
Also, why is there still no hardware tagging to simply prevent memory misuse at cpu level, if it actually is such an important issue?
ijustlovemath · · focus · HN ↗
112233 · · focus · HN ↗
Yet the pitch is that it is needed for the "unsafe" unsafe code, to make it "safe". Not for all code, to make all code safe.