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.<p>I have a notion of purity as well :P<p>I think the applications of this sort of thing are pretty limitless. Maybe rust has `unsafe` but with further verification extensions to the language we can really push confidence in a working, safe product.
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:<p><pre><code> impl List {
#[ensures(self.len() == old(self.len()) + 1)]
pub fn push(&mut self, elem: i32) {
// TODO
}
}</code></pre>
According to the Readme, this is based on a more-general verification framework called Viper, which apparently works for several languages (including Rust): <a href="https://www.pm.inf.ethz.ch/research/viper.html" rel="nofollow">https://www.pm.inf.ethz.ch/research/viper.html</a><p>There also appear to be equivalents of this tool in Python ("Nagini" <a href="https://www.pm.inf.ethz.ch/research/nagini.html" rel="nofollow">https://www.pm.inf.ethz.ch/research/nagini.html</a>) and Go ("Gobra" <a href="https://www.pm.inf.ethz.ch/research/gobra.html" rel="nofollow">https://www.pm.inf.ethz.ch/research/gobra.html</a>).<p>I'll definitely be checking out Nagini for my work!
It doesn't mention unsafe in the README but the website says:<p><pre><code> The first versions of our tools are under development, and target a small but interesting fragment of Rust without unsafe features; in the future, we plan to extend our work to tackle a large portion of the language, including certain patterns of unsafe Rust code.
</code></pre>
I wonder if this can be used to prove that unsafe code is memory safe.
I don't understand how this could work from looking at the readme. It says:<p>> verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable<p>But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint.<p>So if it detects any panic! Then that's amazing. But if it only detects panic for integer operations, we already have that feature. Either way, the overflow/panic! wording is confusing because it either only applies to debug builds or applies to more than integer operations
That's nice. Classic verification. Someday the compiler should do this as part of optimizing run-time checks. Most of the time, either overflow is impossible, or you really needed a run time check.<p>The static analysis I'd like for Rust is deadlock analysis. If you lock things in different orders in different threads, you can deadlock. That is, if thread A locks X, then Y, and thread B locks Y, then X, there is a potential deadlock. Whole-program static analysis can detect that. It's a good check to have, because infrequent deadlocks of this type may pass testing.
What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.
Was a bit disappointed to discover that the advertised Prusti Assistant VS Code assistant sort of silently sits there waiting ("Checking requirements...") if you don't have Java installed.<p>I feel like assuming Java is installed doesn't really fit the audience.
Here's a 2020 overview of Rust verification tools <a href="https://alastairreid.github.io/rust-verification-tools/" rel="nofollow">https://alastairreid.github.io/rust-verification-tools/</a> - it says<p>> Auto-active verification tools<p>> While automatic tools focus on things not going wrong, auto-active verification tools help you verify some key properties of your code: data structure invariants, the results of functions, etc. The price that you pay for this extra power is that you may have to assist the tool by adding function contracts (pre/post-conditions for functions), loop invariants, type invariants, etc. to your code.<p>> The only auto-active verification tool that I am aware of is Prusti. Prusti is a really interesting tool because it exploits Rust’s unusual type system to help it verify code. Also Prusti has the slickest user interface: a VSCode extension that checks your code as you type it!<p>> <a href="https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant" rel="nofollow">https://marketplace.visualstudio.com/items?itemName=viper-ad...</a><p>Now, on that list, there is also <a href="https://github.com/facebookexperimental/MIRAI" rel="nofollow">https://github.com/facebookexperimental/MIRAI</a> that, alongside the crate <a href="https://crates.io/crates/contracts" rel="nofollow">https://crates.io/crates/contracts</a> (with the mirai_assertion feature enabled) enables writing code like this<p><pre><code> #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
fn geeting(person_name: Option<&str>) -> String {
let mut s = String::from("Hello");
if let Some(name) = person_name {
s.push(' ');
s.push_str(name);
}
s.push('!');
s
}
</code></pre>
And have it checked at compile time that the assertion holds! Which is a bit like Liquid Haskell in capability: <a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="nofollow">https://ucsd-progsys.github.io/liquidhaskell/</a><p>... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!! <a href="https://github.com/viperproject/prusti-dev/blob/master/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs" rel="nofollow">https://github.com/viperproject/prusti-dev/blob/master/prust...</a><p>Now I'm wondering which tool is more capable (as I understand, they leverage a SMT solver like Z3 to discharge the proof obligations, right?)