I’m a bit of a dabbler in program verification, and know just enough to be confused about the central idea of this post:
In some sense, the Rust type checker is performing a separation logic proof for us, each time we compile our program.
If these steps are separable in this way (the Rust compiler does half, and the verifier does half), why don’t verifiers work that way? Is it simply because the Rust compiler can reject programs it can’t reason about cleanly?
I’m really attracted to the idea that Rust is easier to verify, both because I like Rust for other reasons, and because I like verification. But, in my ignorance, I’m missing something about this post (and Graydon’s) that explains why the two steps can’t be ahem separated when verifying a language like Java (that is otherwise memory safe but allows aliasing of mutable references).
My understanding is that Rust brings two things to the table relative to, eg Java:
programs already come with modular aliasing annotations. You can imagine augmenting Java with some kind of “this is unique reference” annotations for proofs specifically, but they’ll naturally be much less ergonomic than what Rust has.
more importantly, the programs written in Rust already have nice aliasing properties.
The last one is important and is the real reason why C++ can’t incrementally evolve into Rust.
You can add lifetime annotations with Rust’s semantics to C++ language! What you can’t do though, is adding those lifetime annotations to the actual C++ code you already have, because that code plainly doesn’t conform to the Rust aliasing model. It doesn’t observe shared^mutable.
So, Rust has annotations, that enable modular reasoning, and it forces you to change your source code logic in a way that is more amenable to modular reasoning. The first part you can have in any language. The second part plainly doesn’t work for existing bodies of code.
If these steps are separable in this way (the Rust compiler does half, and the verifier does half), why don’t verifiers work that way?
Footnote 5 says they do:
The first tool to note this was Prusti (2019), which verifies Rust programs in a separation logic verifier but uses typing information to automate the separation logic parts of the proof!
Why does the article say that OCaml poses a problem since it includes the ref type and Rust does not, when Rust has the RefCell type[1] offering the same functionality?
I can see two possible answers: (1) RefCell is not part of the language, but only of the standard library, and is implemented via unsafe, and the whole discussion purely considers safe Rust. (2) RefCell still checks the mutable xor shared access pattern, just only at runtime.
To (1) I’ll answer, real Rust programs pretty much always use some interior mutability (if not via RefCell, then via Mutex–and even channels might pose similar problems?); is the formal verification discussion not interested in real-world programs? Isn’t the distinction between Rust the language and its standard library academic?
To (2) I’d say, you can take short-lived borrows to the RefCell every time you access it, and now it really is the same as OCaml’s ref, isn’t it?
I’m a bit of a dabbler in program verification, and know just enough to be confused about the central idea of this post:
If these steps are separable in this way (the Rust compiler does half, and the verifier does half), why don’t verifiers work that way? Is it simply because the Rust compiler can reject programs it can’t reason about cleanly?
I’m really attracted to the idea that Rust is easier to verify, both because I like Rust for other reasons, and because I like verification. But, in my ignorance, I’m missing something about this post (and Graydon’s) that explains why the two steps can’t be ahem separated when verifying a language like Java (that is otherwise memory safe but allows aliasing of mutable references).
Anybody know the answer?
(ignorant noob when it comes to verification):
My understanding is that Rust brings two things to the table relative to, eg Java:
The last one is important and is the real reason why C++ can’t incrementally evolve into Rust.
You can add lifetime annotations with Rust’s semantics to C++ language! What you can’t do though, is adding those lifetime annotations to the actual C++ code you already have, because that code plainly doesn’t conform to the Rust aliasing model. It doesn’t observe shared^mutable.
So, Rust has annotations, that enable modular reasoning, and it forces you to change your source code logic in a way that is more amenable to modular reasoning. The first part you can have in any language. The second part plainly doesn’t work for existing bodies of code.
Footnote 5 says they do:
Because if they are separated, there can be legal compiled programs that break the rules, so the rules that simplify reasoning… Are not rules!
Why does the article say that OCaml poses a problem since it includes the
reftype and Rust does not, when Rust has theRefCelltype[1] offering the same functionality?[1] https://doc.rust-lang.org/std/cell/struct.RefCell.html
I can see two possible answers: (1)
RefCellis not part of the language, but only of the standard library, and is implemented viaunsafe, and the whole discussion purely considers safe Rust. (2)RefCellstill checks the mutable xor shared access pattern, just only at runtime.To (1) I’ll answer, real Rust programs pretty much always use some interior mutability (if not via
RefCell, then viaMutex–and even channels might pose similar problems?); is the formal verification discussion not interested in real-world programs? Isn’t the distinction between Rust the language and its standard library academic?To (2) I’d say, you can take short-lived borrows to the
RefCellevery time you access it, and now it really is the same as OCaml’sref, isn’t it?