Formally Verifying Rust's Opaque Types | Hacker News Reader

Formally Verifying Rust's Opaque Types

dylanj.xyz

133 pointsBreakfastB0b65 comments

It's always a pleasant surprise to see people using Coq and other formal verification technology to build confidence in their ideas and algorithms. We need to stop producing buggy software! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [2] (a variant of another useful tactic called `magic`) which can automatically prove the theorem from the article.

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

Could TLA+ do the same thing?

A nice intro/showcase to Coq, I suppose. But the triviality of this frankly makes it difficult for me to understand what value this has and what it teaches us - we've just proven that one kind of syntax is equivalent to another, because of an intuitionistic tautology. What I'd like to know is what it would mean for the rust type system if this weren't true, and therefore, what is really the difference between rust opaque types and generics in function signatures other than syntactic, and their formulation?

As someone who's used to functional programming but not familiar with any proof systems, I've sometimes applied Curry-Howard the other way and used Haskell as a primitive proof system by writing the corresponding function (being careful to avoid infinite recursion). GHC's support for "typed holes" makes this pretty convenient - just write a part of the function and leave a hole (_) for the rest, GHC tells you what type is needed there.

The title is a bit misleading: you're not formally verifying rust's opaque types - you're simply proving a intuitionistic logic proposition using Coq. There's nothing Rust specific in that proof.

That’s totally fair, it does make it sounds like I’m verifying the compiler’s implementation of it. However it is proving that making such a transformation between the two styles of static dispatch is always sound.

What would you have titled the blog instead to be less misleading?

Introduction to Coq theorem proving using Rust static dispatch equivalency example

Fantastic article. For auditory learners like me, this is an iconic talk in the OG “Advanced Topics in Programming Languages” series that Google used to do: https://youtu.be/h0OkptwfX4g

It goes all the way from parametric polymorphism, up through Curry-Howard, and winds up at Girard-Reynolds. It was what got me passionate about type theory as a young lad.

I love this walkthrough! It reproduces, in narrative form, the experience of interactive theorem proving. Great exploration of a niche detail.

Author here. Glad you liked it! I’ve had a real fear of writing since High School and so starting this blog is my attempt to work through it.

It’s a shame that more engineers don’t have the time or interest to learn formal verification because it’s really enjoyable once you get the hang of it. Although it rarely directly comes up at work, I think it gives a good framework for thinking in strongly types languages with advanced type systems like Rust, Typescript, or Haskell.

Personally it’s because I don’t enjoy solving the problem once in one language and then transcribing it into a totally different language and worrying I got the transformation correct (+ I still need to write all the same tests). Also, afaik proof languages don’t have libraries for building up more and more proofs, and, even if they did, they’re not going to come bundled with random runtime dependency X I picked to implement it. It doesn’t feel like it will be an enjoyable experience and there’s generally little incentive from the buyer’s end (ie management aren’t typically demanding it / hiring for it / giving time in the schedule to write proofs).

And as far as it helping with other languages, I feel like practical TypeScript understanding doesn’t benefit particularly from proofs. Rust and Haskell I can’t make claims about but if that’s true those languages will suffer (but I don’t think it’s really needed).

I didn't mean to imply that people should be using Coq or another proof assistant in their development workflow. More that understanding formal verification aids in thinking about typed programs.

However no type system of a Turing complete programming language can ever be truly trusted as a proof system because looping forever or other non-termination can be used to prove any proposition.

  const proveAnything = <A>(): A => proveAnything()

The above function can prove any proposition including 1 == 2, by just recursing forever.

However, take Rust's ownership system for example, it uses a type system that corresponds to a kind of logic called a sub-structural logic that denies one of the axioms of typical classical logic systems, namely, the weakening axiom, e.g. a function of the type

  fn <A>(a: A) -> (A, A) { ... }

is not possible to write in Rust, but easily writable in most other programming languages. Because of this, Rust is able to "prove" that the program is free from data races which is pretty cool if you ask me.

Can't the function just return `(a.clone, a.clone())`?

Maybe you mean something like this? `fn extend_vec(to: &mut Vec<i32>, from: &Vec<i32>) { ... }`

This does not compile if you pass the same Vec as to and from, because of the `&mut`

Without a trait bound that demands cloneable items, no.

Before I begin - I hope my comment doesn't come across as too confrontational. I don't want to invalidate your experience, but I'd like to spread information about formal verification techniques that are usable today.

> Personally it’s because I don’t enjoy solving the problem once in one language and then transcribing it into a totally different language and worrying I got the transformation correct (+ I still need to write all the same tests).

Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.

> Also, afaik proof languages don’t have libraries for building up more and more proofs, and, even if they did, they’re not going to come bundled with random runtime dependency X I picked to implement it.

The Archive of Formal Proofs [2] is a collection of Isabelle theories (proof modules) that you can easily integrate into your own proofs. Some proofs in the AFP are about specific properties so they're not that interesting as a proof library, but many others include reusable specifications that are useful in other proofs.

I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.

I'm only familiar with Isabelle/HOL, so my comment is limited to that environment.

[1] https://isabelle.in.tum.de/overview.html

[2] https://www.isa-afp.org/

I didn't mean to disparage your post nor did I intend to come across as angry if that's how it landed (sorry). You just asked the question of "why isn't this done more often" & I was adding my perspective.

> Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.

These languages are not the most commonly ones used in the industry (Java, C#, JavaScript/TypeScript, C/C++, Rust, Python etc). I'm particularly interested in C++ and JavaScript/TypeScript if you know of any.

> I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.

What I was saying is that you may have a distributed system that makes up multiple components. Usually each component individually is already pretty hardened. The errors indeed pop up in the glue code where you're sending messages between those distributed components. Less so about the correct flags in socket creation but "did you remember to handle error case X?", "did you manage the state transitions correctly for distributed messages?", "is the custom caching layer I layered on top of the distributed component interacting correctly with that component?", "did I correctly implement 2PC?", etc. For example, imagine that you used YuggabyteDB. YuggabyteDB may have proofs around its behavior. However, if I want to write a proof for my usage of it, I'm going to have to pick generic components that describe a "distributed database" and customize what kind of isolation level I'm expecting between transactions. Some of this can be expressed generically and maybe there are such components already written. Some of the stuff those is extremely nuanced like "DB X implements operation Y in a nuanced way".

I'm not saying these are all necessary for the purposes of getting value out of type checking. I am suggesting that the difficulty for type checkers to be used in that way, the lack of proof "APIs" for components, the challenge of dictating runtime language auto generation / manually translating is a reason you haven't seen a massive rush towards formal proofs I think.

> It’s a shame that more engineers don’t have the time or interest to learn formal verification

That's the problem with CS, which is full of beautiful and intriguing topics. Graph theory, game theory, formal logic & semantics, automata, compiler design, theorem proving, type theory, computational social choice, resource allocation, coding theory, cryptography, distributed computation, etc..

Absolutely! Every time I think there's a boring area of Computer Science when I read more deeply into it, it turns out to be amazing. Even something which I hated in University like Complexity Analysis turned out to be utterly fascinating after I read Scott Aaronson's "Quantum Computing Since Democritus". It has such deep and interesting connections to ontology, epistemology , and physics. So much to learn, so little time. Gotta keep that story point velocity up!

Nice writeup, been a while since I had used coq, it was nice to try and work it out from memory, but be able to refer back to your post when I got stuck.

Also threw together a tiny lean proof without tactics, figured i would post a link to it to avoid spoilers. https://gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c425...

couldn't get the link to work in the lean-web-editor though.

I'm having some trouble understanding the article's formula; and honestly it's a little weird to see people complain about how trivial the proof is.

Both this article and the article it quotes introduce the "((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q))" formula with absolutely no additional explanation. I guess that's fine if the article are meant for people with a mathematics background, but at someone who has always struggled with post-high-school-maths... what the hell?

I understand what ∃, ∀, ⇔, and → represent ("there exists", "for all", "equivalent" and "implies", respectively), but I have no idea how to parse the entire formula. What are P and Q?

After multiple tries, I'm reading it as "saying that 'there exists a x such that P(x) is true' implies Q" being equivalent to "for all x, P(x) implies Q", with the idea that P and Q are arbitrary proposals or whatever the proper terms are... But still, just processing the logical reasoning in my head is tough.

On the other hand "some types implement traits, and if a function expects a trait impl you can only pass it types that implement that trait" feels absolutely clear to me. It might be that Rust is good at breaking down math concepts into the essentials you need for programming. Or it might be that formal Math notation is not for me.

Just a quick note, the symbol ⇔ is typically meant to stand for 'material implication' and would be better read as 'if and only if'. Or at least that is the 'normal' usage in the literature for intuitionistic logic. It doesn't really change your reading of it, but equivalent does not really capture the traditional meaning of material implication. It is more accurate to portray the logical sentence as valid with either implication in the first position. The two statements are not equivalent to each other, but the re-ordering of the implications would be, i.e.

((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) is equivalent to (∀ x. (P(x) → Q)) ⇔ ((∃ x. P(x)) → Q)

P and Q are propositions. P takes one parameter and Q takes none. For example P(x) might be "x is odd". The term `P(x)` by itself refers to P(x) being true.

So `∃ x. P(x)` is read as "There exists an x for which P of x is true." or "There exists an x such that P of x is true."

So `((∃ x. P(x)) → Q)` is read as "If there exists an x such that P of x is true, then Q is true."

And `(∀ x. (P(x) → Q))` is read as "For all x, if P(x) is true then Q is true."

The `⇔` indicates that the left hand side is true if and only if the right hand side is true, or in other words that they're equivalent, which you can tell from the descriptions above that they are.

> Or it might be that formal Math notation is not for me.

No, it just means that you haven't studied that notation. Like programming, being skilled at maths is not something you're just naturally gifted with. It has to be studied.

The proof of the proposition in question is "trivial" in the sense that a first course in formal logic is more than enough to fully understand it, and that there is really no extra trick involved, basically the proof is as straightforward as it could be.

I will agree that the article doesn't explain enough how the formula in question relates to type theory and Rust's type system in particular.

Thanks for the feedback, I should have spent more time connecting the logic statement to the equivalent rust syntax as you’re right the post has a weird audience problem otherwise. You either already know logic well enough that the proof is trivial, or it doesn’t make any sense.

I've been thinking for some time that one of the key advantages of Rust's safe/unsafe code will turn out to be that formal methods can be applied to the unsafe parts.

Safe Rust is truly safe if it only calls safe Rust or if all the unsafe code is correct.

And safe Rust is a little too inflexible to do certain things, so the unsafe word is a necessary evil. But turns out it's not a bug, it's a feature because now you can trivially identify which parts of the codebase require extra scrutiny to avoid memory corruption and data races.

With FM the main downside has always been the added cost and development time/complexity, needing to use obscure academically oriented systems that most developers have no experience with, etc. But that complexity is probably okay for a project like the Rust standard library, which is already a highly complex project and will only be majorly worked on by a relatively small subset of Rust developers. So you could save some of that cost by only needing it in a (relatively) small part of the ecosystem.

Ofc I realise this wouldn't give the same level of correctness as doing all code with FM. You could only verify whatever guarantees Rust provides for code with no unsafe codepaths. And proofs can have bugs too. But still I think it could increase safety a lot.

The Rust standard library is quite big, not compared to Python obviously, but compared to the scale of things we'd usually apply formal methods to.

It also relies heavily on stuff that's not Rust. For example it's one line in Rust to decide to suppose this whole file named "C:\myfile\stuff.txt" is UTF-8 text, so put it all into a String - the standard library reflects the obvious ways that could fail, maybe there is no such file, maybe it's actually a JPEG and not UTF-8 text, maybe the file is so enormous it can't be represented in RAM on this (presumably 32-bit) computer - but it's relying on the operating system to actually have a working filesystem, you can't use formal methods to deal with such things.

It could make more sense to do the same to Rust's core library: https://doc.rust-lang.org/core/

Unlike std, core is mostly stuff the language itself assumes exists. Rust's fundamental types all have methods for example (e.g. 'x'.is_ascii() is true) unlike say C, and the implementation of (most of) those methods lives in core.

Well, core is clearly the place to start, otherwise anything above it in the lib hierarchy would be on non-verified ground anyway. I think it would then be worthwhile to at least start on the alloc crate. A lot of the datastructures use quite a few unsafe concepts for optimisation and getting around the borrow-checker without having to resort to runtime checking. Formally verifying Vec, Hashmap and friends would obviously pay huge dividends across the entire rust ecosystem in terms of overall safety, and should be perfectly surmountable(at least modulo the behaviour of OS memory management). And there's no reason you couldn't do it module by module.

I doubt it. Formal verification helps you prove your algorithms are correct. Bugs from unsafe rust are going to be way more subtle than that, like accidentally assigning a string and crashing [1].

[1] https://lucumr.pocoo.org/2022/1/30/unsafe-rust/

The manual proof style was nice to see for pedagogical purposes, however it should be noted that the statement is just a intuitionistic tautology, so much so that the entire proof can be automated with the built-in firstorder tactic:

  Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
      ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
  Proof.
    firstorder.
  Qed.

On a somewhat technical note, I think the author is being slightly imprecise, though in a way that will normally not trip up most people. The proof has to be understood either as a proof scheme in first order logic, in which case we technically need a separate proof for each possible choice of predicates P and Q, or we have to implicitly quantify over P and Q, i.e. "for all P, for all Q", which leads us to second order logic, but in this case there is now a single proof (which is exactly what's the case when we're using Coq).

At least that's the case in classical logic (which is enough to understand this article), I'm not knowledgeable enough about intuitionism to know whether it typically includes second-order quantification, but even in that it would probably be better to make the quantification explicit.

Michael Clarkson of "OCaml Programming: Correct + Efficient + Beautiful" [0] fame is currently publishing series of lectures "Software Foundations in Coq" [1] (new ones appearing once a week?) as a companion to [2] which looks as great as OCaml series.

[0] https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b...

[1] https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk...

[2] https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.h...

Just noting that the statement in question is not only a valid proposition in intuitionistic logic, but also in classical logic. That's not really surprising, as classical logic can prove everything that intuitionism can prove, but it deserves to be called out, as it otherwise might seem more sophisticated than it is for people unfamiliar with the finer details of proof systems.

Personally, I find the title to be slightly misleading as the proof is essentially just (un)currying for dependently typed function.

I’m not sure I understand the connection to dependent types, would you be able to elaborate?

Normal currying describes an isomorphism between functions of type (A x B) -> C and functions of type A -> (B -> C). With dependent types, we can have an isomorphism between functions of type ((a : A) x (b : P(a))) -> Q(a, b) and functions of type (a : A) -> ((b : P(a)) -> Q(a, b)). What your article proves is a bit less generic with Q doesn't vary accoring to a and b; i.e. an isomorphism between ((a : A) x (b : P(a))) -> Q and functions of type (a : A) -> ((b : P(a)) -> Q).

Yeah that makes sense, thanks for explaining.

I don't want to make it seem like I'm proving anything novel here, the proof I work through is definitely pretty basic as far as proofs go. It's written somewhat narratively because it reflects a train of thought I went through a few days ago when reading about existential types in Rust. Seeing the theorem ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) in the blog post made me want see if I still remembered enough Coq to prove it, and then when I was sitting down this morning to write something I thought it would make a good blog post as it explores some deep cuts of what I've been learning in Rust and might make a good introduction for people into Coq. I'll definitely take it on the chin that I titled the blog too ambitiously however and I'll be more modest with my titles in the future.

Regardless of the verification bit (which I didn't read, as it's a bit over my head), this is probably the best explanation I've read about the difference between `imp Trait` and `dyn Trait`.

I have been contemplating on learning TLA+. Could someone experienced with formal verification let me know what I could be missing by not learning something like Coq?

Reply on news.ycombinator.com