Having worked on program verification in the past, Rust looks like the most useful modern language to which formal methods can be applied. Rust's rules eliminate so many of the cases that are hard to formalize.
Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can't fail, you can eliminate most reference counts. That gives you free interior mutability when that's possible.
The author's comment on provers is interesting. The big problem with theorem provers is that they're developed by people who like to prove theorems. They're in love with the formalism. This leads to a UI disconnect with programmers.
You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.
Machine learning may help in guiding theorem provers. Most programs aren't that original in terms of control flow and data usage. So inferring a proof plan from other code may work.
ML systems can't be trusted to do the proof, but may take over guiding the process.
F* is this mythical language that proves stuff automatically (with an SMT solver, more powerful than SAT), but still lets you prove manually if the automated solver fails
The crypto routines in Firefox and Wireguard is actually written in F* (or more specifically Low, a low level DSL embedded in F), not in Rust, and is fully verified
> You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.
Agreed, though I think Lean is making big progress in the UX front of ITP verification through its extensive meta-programming facilities.
My issue with these tools applied to verifying external languages like Rust, is that the proof is not written in the target language, forcing your developers to learn two languages.
I have recently been thinking about what a "verification aware Rust" would look like, colored by my experience writing Creusot, the work on Verus and Aeneas and my time in the lab developing Why3. I think building such a language from the ground up could provide a step change in ease of verification even from Rust, particularly with regard to those "hard parts" of the proof.
> "verification aware Rust" ... building such a language from the ground up could
Could you sketch in a few bullet point what you think is missing and how to fix the gaps?
In my experience a core problem is that adding rich specifications slows down rapid evolution of programs, since the proliferate transitively along the control flow graphs. We can see this most prominently with Java's checked exceptions, but most effect annotations (to give an example of simple specification annotations) suffer from the same cancerous growth. This is probably at least partly intrinsic, but it could be improved by better automation.
> Could you sketch in a few bullet point what you think is missing and how to fix the gaps?
Not yet, I am planning on writing some blog posts about it but there are still enough fuzzy points I don't want to share yet.
> ... since the proliferate transitively along the control flow graphs. ... suffer from the same cancerous growth.
This is one of the biggest and most difficult issues of verification, I fully agree. The 'promise' of verified code is that you don't need to understand the code, you can just look at the smaller, higher-level spec, but right now verified code has a specification & proof overhead > 1, it needs to drop to < 0.1 for it to become economical.
Yes, keep plugging on that one. Verification statements should be in the same language as the program, and be syntax and type checked on every compile.
Not in comments. That keeps them consistent with the code.
Sorry that this is a very basic question but I never had any of this in uni and I find it super exciting:
If I am trying to prove something I can state in my target language how would statement and proof differ?
If the thing to prove is not expressible in the target language (e.g. the fact that a function terminates) I would have to use a separate language anyway.
Could you give an example how this could hypothetically look like (preferably in pseudo Rust)?
1) you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized. So you want to state that they always produce the same thing.
fn my_complex_algo(x : Input) -> o:Output ensures o == simple_algo(x)
2. You might have high level "properties" you want to be true about your program. For example, a classic property about type-checkers is that they are "sound" (meaning that if you say a program is well typed, then when you run it it must be impossible to get a type error).
3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.
To me at least, the most difficult part of verifying rust code has been the lack of any pre/post conditions on the standard library, I quite often have ended up rewriting chunks of the std library, pulling them directly into my program to verify them.
I personally think it would be interesting if we had a nightly-only/unstable pre/post conditions in the std library. Then one could take the commit of the compiler that corresponds to a stable release and verify against that. That is the overhead I seem to be bumping my head against whenever I try to verify some rust code at least.
Since learning Eiffel in the 90's I keep looking forward for them to become mainstream, beyond the typical assert like statements.
So far we had annotations in Java (which required additional tooling and never took off), .NET (hidden behind enterprise license, thus hardly adopted), D (which suffers from adoption), Common Lisp (nice, but again adoption issues), Ada (again the language adoption), C++26 (if they actually land, and only as MVP)
Almost 40 years later, and still no good story for DbC.
I think that Coq/Agda/Lean and friends are really going to be the winners in the proof space. Interactivity is a pretty good model for the feedback loop, and they're systems that exist and work, without a lost of asterisks.
The biggest thing I think these tools are missing out of the box is, basically, "run quickcheck on my proof for me". It's too easy to have some code, and try to prove some property that isn't true, and rip your hair out thinking "why can't I get the proof working!"
If halfway through your proof you end up in a thing that seems nonsensical, it would be nice for these tools to just have a "try to generate a counter-example from here" command that spits out a thing.
Proofs are so path-dependent, and it's not trivial to do in general. But I think they are all very close to greatness, and every time I've gone through the effort to formally verify a thing, it's been pretty illuminating. Just... if you're trying to prove some code, the process should take into account the idea that your code might be buggy.
I also quite like Idris, the problem with these languages is that they require being a Mage level 10, while most folks are still getting around magic exists.
Most programmers don't have enough previous experience proving things so this is unnatural for them. It is sadly impossible to require programmers to have been a math major to get them the mental facility to work with these languages.
At my university, all majors of computer science have to take a course in discrete math, which involves writing a couple different types of math proofs using proof by induction (including strong induction) and proof by contradiction. However, that was the only class I've ever taken where I've had to write proofs regularly.
Anyway, I think that, at a minimum, at least one class like that should be part of every CS major's education, if it isn't already. That way, proofs are less intimidating, and things like Coq and Isabelle/HOL are less intimidating.
I agree with you, but the ship has sailed to retroactively require all programmers to have such experience. Also, the typical introductory discrete math course likely doesn't require writing proofs in a language precise enough to be formalized. I would think that we need at least one more introductory course to logic (first order logic, Peano axioms) and an introductory course to type systems (structural induction, progress and preservation, etc).
We also learned some first order logic, enough to write the proofs in formal language, though we didn't learn anything about type systems.
You're probably right about the ship having sailed, though. It's probably harder to get people to learn new things when they haven't been in school for a long time.
In my case (Lean), I've been getting a lot of help through the Zulip community. There's a dedicated #new_members stream where anybody can ask total beginner questions. It's quite humbling actually when you have someone like Kevin Buzzard answering your noob questions.
I'm sure other solvers (Coq, Idris, etc.) also have online communities where you may be able to ask questions.
I'll have to agree with this. In particular, there always seems to be some stage where you'll have to think carefully about how the simplifier works exactly, about different types of equality (syntactic vs. definitional vs. provable), etc. And changing internal representations of objects will also mean that old proofs might not compile anymore. And tactics are often rather opaque blackboxes.
I say this as a non-expert who has been enjoying writing some Lean recently and has previously also written some Coq and Idris.
Isabelle/HOL has Quickcheck, which is precisely what you think it is. Although it only works if the free variables in the thesis you'd like to prove are sufficiently simple AFAIK (think integers or lists). The more powerful alternative to Quickcheck is Nitpick, which is a purpose-built counterexample finder.
The workflow you'd like already exists one to one in Isabelle: You can simply type "nitpick" halfway through a proof and it will try to generate a counterexample in that exact context.
> "try to generate a counter-example from here"
For the theories behind some SAT solvers, that's quite possible. There's a set of problems that are completely decidable. These are composed of add, subtract, multiply by constants, logic operators, and theory of arrays and structs. That covers most things which cause programs to crash and many of the things you want to write in assertions.
> Machine learning may help in guiding theorem provers
Interesting idea. There would be real upside where the machine learning system gets it right and guides the prover to a valid proof, and little downside if it gets it wrong. (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property.
> (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property.
Don't basically all applications of any heuristic solver to NP problems have this property? (Including problems that are only in NP, because they are also already in P.)
Yes, sure, I could have phrased that better. There are no doubt many possible applications of the idea. The recent headline-grabbing applications of machine learning tend not to be like this.
Though even amongst the recent-headline-grabbing stuff there are some areas that you can improve at by the equivalent of AlphaGo's self-play. Basically, when you have a slow and expensive option to use a weaker version of your system to produce better decisions / smarter data, and then use those to train the system.
> Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can't fail, you can eliminate most reference counts. That gives you free interior mutability when that's possible.
I’m not a formal verification guy, but I don’t think locks in the traditional sense is helpful. No compiler will give you anything useful to work with wrt locks. You just accept and live with the danger.
In fact, locks and ref counts are runtime constructs in Rust. Imo it “goes against” even Rust’s own strong principles of single ownership - these things are shared mutable state. Arc broke Rusts RAII model so much that they had to remove scoped threads (which needs destructors to run before end-of-scope).
Anyway, rust aside. Global refcounts have cyclic and leak issues that again are global. I don’t think we can necessarily get rid of them, but I do believe containing them is better, eg with arena-style scoping.
As for locks my gut feeling is we need an asymmetric data structure, for instance a channel. In eg Go you can break a channel into sender and receiver, and have the sender goroutine do `defer close(ch)` which is guaranteed to run if the rest of thread finishes, even if there’s a panic. Doesn’t necessarily have to be channels but separating the roles (reader-writer / producer-consumer) is much easier to reason about, and that probably helps formal analysis too.
Scoped threads have been reintroduced to Rust since ver 1.63, released in August 2022. There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run - however the changes required for that are large and will probably have to be introduced in a new Rust edition.
Unfortunately rust language development has practically ground to a halt. There is a trickle of work but it’s highly unlikely that major language features will happen any time soon.
I'm not sure what you mean. There are fewer flashy announcements for things that block people, but development continues unabated, with large refactors that enable things that weren't possible before. Things like Return Position Impl Trait In Traits, Derefs in patterns, a new trait system checker, enhancement to const eval, generators and that's just of the top of my head. Not everything is gonna land soon, but development is happening. The major language feature work is happening, they just are large enough or contentious enough that stabilizing them will take time.
Oh please, they’ve landed a few nice things but larger items like generators are likely not coming soon.
Just look at the async roadmap for example, how many years has it been and how much progress has been made?
As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it. I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday”
> landed a few nice things but larger items like generators are likely not coming soon.
Generators got blocked on settling AsyncIterator/Stream. The work for it is happening. It's taken too long, but not because people are sitting on their thumbs.
> Just look at the async roadmap for example, how many years has it been and how much progress has been made?
Hard things are hard and take time.
> As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it.
You can say whatever you want to say, everyone can. But expect pushback from the people pulling the cart when you state that the cart isn't moving just because it isn't moving as fast as you want in the exact direction you want. Just take a damn glance at the review queue, or even the release notes. A ton of work is being done, of different levels of difficulty and the things that aren't stabilized quickly is because they have research-level open questions.
> I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday”
I don't know why you read that as passive-aggressive, but I certainly see your reply as dickish.
If the cart is moving slowly I’m going to point out it’s moving slowly. If you want to take that personally that’s your problem, but I’d prefer to be honest about the situation.
The fact of the matter is significant language features have stalled. And comments like the one i quoted are passive aggressive when you consider they’re casting doubt on whether certain language features will ever see the light of day.
It’s especially disheartening when you don’t really hear much from the language team and it doesn’t seem like progress is being made on these language features.
GGP here. I think you’re both right. As a formerly involved contributor I can assure you that there are legitimately hard problems, and that there are very bright people working on it.
However, the reason why it’s so hard, is imo because Rust matured itself so quickly, by basically having a bunch of 10x mega brains lay a foundation of insufficient but unchangeable features and then leave a lot of details to be solved later when (a) there are much more people and stakeholders involved and (b) there are much more promises made around governance, stability etc. And, as it turns out, laying the “remaining pieces of the puzzle” is harder, especially if you’re not allowed to move the initial pieces.
This in turn creates an incongruence for outside observers, where it appears like development is slower (which is true) because people are incompetent/lazy/prioritize badly (which is not true).
The mistake here, in my humble opinion, is moving ahead so quickly many years ago. Async is the perfect example of this, but as I alluded to earlier, I think allowing leaks was a similarly rushed decision, and that was much earlier. If I were to bet, people were excited about maturing the language for production, but, since there was sooo much uncharted territory, there were novel subtle challenges which during the frenzy appeared like they could be solved quickly with brainpower alone to meet the deadlines and keep the excitement going. But even the wrinkliest of brains can’t deduce the implications of 4th order effects down the line - you have to try it out and build real life things. You have to be humble, when everyone else isn’t.
By what benchmark is it moving slowly, and are you qualified to make that judgement? You might be quite correct, but I don't have enough context to know what role you've played and without context you're coming across as "being loud and obnoxious on the Internet" which isn't (I think?) what you're aiming to be.
The reason I think this has low changes of landing has little to do with the rust developers as the complexity of the feature and the invasiveness to the ecosystem.
I mostly agree with your sentiment, but at the same time I remember being quite skeptical of the possibility of Rust getting async/await at all because I saw no way around the lack of immovable types in the language, and I thought it would be way to disruptive to add it. And then Pin came and allowed to work around that issue (don't get me wrong, Pin is a dirty hack and I hate it, but at least it works, even if it makes tge ergonomics questionable for some use-cases…).
Since then reserve my judgment on stuff I think to be impossible.
Right, but those are a mere shadow of what they used to be, which was JoinHandle with a lifetime parameter. You can’t build a thread pool or async runtime with static borrowing across tasks, which makes the use case very narrow.
> There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run
I’m glad to hear that. I’ve always hoped it’s possible to introduce non-breaking through a new auto trait but there are many delicate details around unwinds and such that may be gnarly. As well as an accumulated dependence on Arcs in library code.
> I’m not a formal verification guy, but I don’t think locks in the traditional sense is helpful. No compiler will give you anything useful to work with wrt locks. You just accept and live with the danger.
Deadlock analysis is well understood. You have to prove that locks get locked in the same order regardless of the path taken. That can be easy or hard. In many cases, if you have the call graph annotated with where locks are set and cleared, you can try to prove that the program is deadlock-free. I'd like to see Rust tools to help with that.
Right, but that’s a global property of everything that uses the lock, so if you’re writing a library you'd have to run the analysis against real or synthetic call graphs. Plus it’s very easy to accidentally break that property if you’re not using it in an analysis-friendly way, no? Instead, role-separated data structures like eg channels, run-once-functions and atomic value swaps can - due to their constraints - make them harder to use in ways that break analysis, and can be analyzed locally.
Say eg my library is acting as a producer. Ideally I can check that I am producing 0-N items and that it closes the channel. Analyzing the consumer can be deferred and decoupled, which is good because it may not exist yet.
The issue with SAT/SMT for program verification is it's too much like dark magic. It's acceptable if you can have it generate a proof certificate for the properties you care about and commit these with the Rust source code - but AIUI, generating usable proof certificates for 'unsat' proofs is a hard problem where you might be better off writing out the proof interactively.
Having worked on program verification in the past, Rust looks like the most useful modern language to which formal methods can be applied. Rust's rules eliminate so many of the cases that are hard to formalize.
Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can't fail, you can eliminate most reference counts. That gives you free interior mutability when that's possible.
The author's comment on provers is interesting. The big problem with theorem provers is that they're developed by people who like to prove theorems. They're in love with the formalism. This leads to a UI disconnect with programmers.
You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.
Machine learning may help in guiding theorem provers. Most programs aren't that original in terms of control flow and data usage. So inferring a proof plan from other code may work. ML systems can't be trusted to do the proof, but may take over guiding the process.