Verus is a tool for verifying the correctness of code written in Rust
verus-lang.github.io
Verus is a tool for verifying the correctness of code written in Rust
1–10 of 16 posts
Re: Verus is a tool for verifying the correctness of code written in Rust
#2Oh hey I worked on this :)
Re: Verus is a tool for verifying the correctness of code written in Rust
#3I 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.
Re: Verus is a tool for verifying the correctness of code written in Rust
#4Re: Verus is a tool for verifying the correctness of code written in Rust
#5Clippy 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.
I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
Re: Verus is a tool for verifying the correctness of code written in Rust
#6I 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
Re: Verus is a tool for verifying the correctness of code written in Rust
#7[deleted]
Re: Verus is a tool for verifying the correctness of code written in Rust
#8I 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.
Re: Verus is a tool for verifying the correctness of code written in Rust
#9I 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 didn’t read OP as saying “the community won’t allow” but more “the tooling doesn’t allow” for what they want to do.
Re: Verus is a tool for verifying the correctness of code written in Rust
#10Clippy 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. I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
I have written complex proofs for distributed system using verus which are certainly not expressed by clippy