3 ms·
> 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 rus
by 112233 18d ago
> 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?
- ijustlovemath 18d agoWhat exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas
- 112233 17d agoObjection 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.