Hacker News Reader

> 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?

View on HN

What exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas

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.

Reply on news.ycombinator.com