Oh, that takes me back to 1982.[1] This is very similar to what we did back then.
The syntactical approach is almost identical. It's much more programmer-friendly than
some other approaches. One of the problems with proof of correctness is that the people
doing it tend to fall in love with the formalism, and it all becomes too abstract and hard.
This project didn't do that.
It's not clear what they do when they need to prove something beyond what an SMT solver can do. That's supposed to be covered in section 11.4, "forall and exists: writing and using triggers, inline functions". What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
That's the right approach - use an SMT solver for the easy stuff, which should be 90-95% of the proofs. Then use something else for the hard stuff. We used the Boyer-Moore prover, a predecessor to the ACL system. Others have used proof-checkers, and Lean. There's recent interest in using LLMs to drive something like Lean; the LLMs make mistakes but the proof checker catches them. Looks like they haven't gotten to this part yet.
The way to partition the problem is to use two "assert" statements in succession.
An assert statement is a proof goal before the assert, and is assumed true after the assert.
So when you hit something hard, you try to bracket it with
assert(a);
assert(b);
and get everything to verify with the SAT solver except
a implies b
Now you have a self-contained expression to prove by some external means. Often you can prove such statements in a generic form, and reuse the proofs.
There should be object invariants, except that Rust doesn't have objects.
It does have structs with associated functions and encapsulation.
You need some way to express that structs with internal state are consistent before and after being called.
C++ has about the right amount of hiding ("abstraction") for this, with public and private fields and functions for objects. Rust's idea of "private" means "same module", not "same struct". So invariants would apply to a module. Then you have to be very organized about when control enters and leaves the module. Like not calling pub functions from inside the module, because the module invariants may not be valid at internal entry to a pub function.
The extensional equality thing is interesting. It needs more description. The basic problem is this: for some types, such as sets, hash tables, and such, objects are supposed to be considered equal if you can't tell from the outside that they're different internally. Formally, the type must have the property
for all functions f where x is an element of T,
x == y implies f(x) == f(y)
That has to be proven for all functions which accept T. Then you can treat type values as equal even if their internal representation is different. Such types can't have any access functions or pub variables which allow you to examine the internal state. For example, if you convert a set to a vector, it has to be sorted, so that you can't tell what the internal order was.
> What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.
The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.
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.
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.
Oh, that takes me back to 1982.[1] This is very similar to what we did back then. The syntactical approach is almost identical. It's much more programmer-friendly than some other approaches. One of the problems with proof of correctness is that the people doing it tend to fall in love with the formalism, and it all becomes too abstract and hard. This project didn't do that.
It's not clear what they do when they need to prove something beyond what an SMT solver can do. That's supposed to be covered in section 11.4, "forall and exists: writing and using triggers, inline functions". What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
That's the right approach - use an SMT solver for the easy stuff, which should be 90-95% of the proofs. Then use something else for the hard stuff. We used the Boyer-Moore prover, a predecessor to the ACL system. Others have used proof-checkers, and Lean. There's recent interest in using LLMs to drive something like Lean; the LLMs make mistakes but the proof checker catches them. Looks like they haven't gotten to this part yet.
The way to partition the problem is to use two "assert" statements in succession. An assert statement is a proof goal before the assert, and is assumed true after the assert. So when you hit something hard, you try to bracket it with
and get everything to verify with the SAT solver except Now you have a self-contained expression to prove by some external means. Often you can prove such statements in a generic form, and reuse the proofs.There should be object invariants, except that Rust doesn't have objects. It does have structs with associated functions and encapsulation. You need some way to express that structs with internal state are consistent before and after being called. C++ has about the right amount of hiding ("abstraction") for this, with public and private fields and functions for objects. Rust's idea of "private" means "same module", not "same struct". So invariants would apply to a module. Then you have to be very organized about when control enters and leaves the module. Like not calling pub functions from inside the module, because the module invariants may not be valid at internal entry to a pub function.
The extensional equality thing is interesting. It needs more description. The basic problem is this: for some types, such as sets, hash tables, and such, objects are supposed to be considered equal if you can't tell from the outside that they're different internally. Formally, the type must have the property
That has to be proven for all functions which accept T. Then you can treat type values as equal even if their internal representation is different. Such types can't have any access functions or pub variables which allow you to examine the internal state. For example, if you convert a set to a vector, it has to be sorted, so that you can't tell what the internal order was.Nice work. Keep plugging.
[1] https://animats.com/papers/verifier/verifiermanual.pdf
> What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)
A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.
The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.
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 didn’t read OP as saying “the community won’t allow” but more “the tooling doesn’t allow” for what they want to do.
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 :)
I wonder whether this could be used as an additional guardrail for LLM coding
https://github.com/verus-lang/verus
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.
I have written complex proofs for distributed system using verus which are certainly not expressed by clippy