Hey Rustaceans,
You may have read my previous post on my masters thesis on program verification in Rust. Well, I've since successfully defended my thesis, so here you go:
I've mostly been back at working on the theorem prover, Lean, itself since then, but I may very well pick up this project again in the future as soon as start my PhD in... *checks watch* oh, tomorrow!
Awesome! One thing, though - in reading through it, the signature of the WhyML in the "Related Work" section doesn't seem to match the Rust code you give.
The Rust you give is:
fn get_mut<T>(slice: &mut [T], index: usize) -> &mut T
while the WhyML is
let get_mut (a: array (ref int)) (i: int) : ref int = a[i]
let get_mut (a: array int) (i: int) : ref int = ref a[i]
However (depending on the semantics of WhyML, which I am not familiar with), those seem like they'd be more similar to the following:
fn get_mut(a: Rc<[&mut i32]>, index: usize) -> &mut i32;
fn get_mut(a: Rc<[i32]>, index: usize) -> &mut i32;
and that a more accurate analogy might be
let get_mut (a: ref (array int)) (i: int) : ref int = ref a[i]
(Which would still return a copy, thus preserving your point that WhyML does not permit all of the niceties that Rust's references do).
These definitions weren't meant to be equivalent — "For example, the first of the following two WhyML functions fails to type check […] In contrast, Rust can provide a perfectly safe function with this functionality".
@valpackett: The distinction I'm making is that there is a spurious difference, namely that while the Rust function mandates unaliased access to the whole slice, the WhyML functions do not - and instead use an "array of unaliased references", or even merely an array of integers. This obscures the point that "this function (signature), which types in Rust, cannot be implemented in WhyML."
IIRC (yeah, maybe I should have described WhyML in more detail), array already implies both indirection and mutability and is subject to the same aliasing restriction as ref, so nesting them like this doesn't buy you anything. Curiously, I can't even get it compiled on Try Why3. The original WhyML paper doesn't talk about the aliasing restrictions at all, unfortunately. The best description I could find is this mailing list post: https://lists.gforge.inria.fr/pipermail/why3-club/2014-January/000890.html
Very impressive stuff. A couple of questions:
The HoTT support in Lean has been removed and won't be coming back, see this recent mailing list post: https://groups.google.com/d/msg/lean-user/90_nKwp-euU/LpRIIZBwDgAJ
While HoTT is gone in Lean 3, as @cmr mentioned, my thesis was still written in Lean 2. My work is mostly constructive, except for the loop combinator, which has to "solve" the halting problem after all. I've never really familiarized myself with HoTT, but I don't think there are many benefits to using it for topics such as program verification.
[quote="tupshin, post:6, topic:9704"]
2. Any thoughts on gradual deeper integration with rust, so that over time whole subsystems and entire crates could get proofs?
[/quote]What kind of integration are you thinking of? You could totally use the tool to verify arbitrary crates right now (as long as it's in the supported subset of Rust), it's just that you would probable need to verify sizable portions of the standard library first, and of course that verification takes some huge time and effort in general (hopefully less so in a future version using Lean 3).
Thanks for the perspective on #1.
Regarding deeper integration, some semi-random throughts:
cargo lean-verify would recheck against any changes to the rust codeI think that Rust shines and can fill a niche as being a high performance, high security language. Which is a big niche and point being security is extremely important for Rust to succeed.
Which makes this one of the most important Rust projects I've seen yet.
Personally I would do a search of cargo to find the most used core Rust functions and one by one starting from the most used verify them and train some other people to help out.
Might even be able to get some kind of Mozilla grant or something for it.
Congrats on the great work! Keep it up!
Plus they also have bug bounties if you find something and there are a bunch of companies using Rust who might happily chip in something, maybe even programmers toward the effort:
I would particularly talk to the companies where security is a priority.
Wouldn't formally verifying the standard library first require a formal model of the unsafe code semantics?
Thanks for the grant suggestions 
. I don't know what shape my PhD program will take yet, but it may be hard to get publications out of "just" doing verification work - except when they necessitate coming up with novel ideas, of course.
Thanks, those are some nice suggestions for attacking the problem at scale. For the modest number of current verification proofs, I was thinking about a simple approach like having a nightli.es hook check daily that everything is still working. But for that I'd first have to update my project to link against a recent rustc that can actually build the nightly stdlib (which usually breaks everything in my code).
Verifying "the standard library" isn't a very realistic goal anyway, I'm afraid. You would usually start with a single function or data structure whose correctness you're interested in and then choose to prove or simply assume the correctness of each of its dependencies - if the dependency uses unsafe code, you will have to do the latter. Correctness proofs will always be dependent on some unproven assumptions (axioms) until we have a verified Rust compiler.