I wonder whether this could be used as an additional guardrail for LLM coding
6r17 4 hours ago [-]
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
mirashii 3 hours ago [-]
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.
11 minutes ago [-]
scott_w 2 hours ago [-]
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.
suobset 5 hours ago [-]
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.
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.
I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
Kab1r 1 hours ago [-]
I have written complex proofs for distributed system using verus which are certainly not expressed by clippy
Rendered at 08:15:52 GMT+0000 (Coordinated Universal Time) with Vercel.
I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.