I tried it not long ago - it's really cool just a tad sad that the rust eco-system didn't allow verus to be more streamlined in the tool and requires these little shenanigans with a different build of it - it felt a bit clunky to swap cargo for the verus one ; but the tool is definitely needed right now
Do you have any reference to the Rust community “not allowing” something? This seems more like a case of a relatively niche tool doing what it needed to do to work, but not (yet) some broader effort to upstream or integrate this into cargo or rustup. I couldn’t find any RFCs or anything, for instance.
I just attended a talk at Northeastern (Boston) on Verus, it's genuinely amazing. I have been using it on my own Rust codebases for a while, and it has made me think deeper about the structure and semantics of Rust code.
Oh hey I worked on this :)
<a href="https://github.com/verus-lang/verus" rel="nofollow">https://github.com/verus-lang/verus</a>
Clippy with unstable features enabled catches most if not all of these cases automatically? This seems like it needs more work to do the same thing clippy does.<p>I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.