That looks incredibly useful. Proving the absence of panics and overflows is already great, and with the annotations you can guarantee properties you'd normally write property tests for, like in this example from the docs: impl List { #[ensures(self.len() == old(self.len()) + 1)] pub fn push(&mut self, elem: i32) { // TODO } }
This really reminds me of design by contract, which I find absolutely fascinating.
Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods. In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of ab…
Sounds really exciting! Mir interpreter has the same limitation. Have you examined incorporating mir in your analysis?
Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.
This is great. I'm building something similar, an effects system for rust, and it looks quite a bit like this. The difference is that my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time. I have a notion of purity as well :P I think the applications of this sort of thing are pretty limitless. Maybe rust has `unsafe` but with further…