from Hacker News

Formally Verifying Rust's Opaque Types

by BreakfastB0b on 8/1/22, 11:42 AM with 65 comments

by stepchowfun on 8/1/22, 1:56 PM
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...
by homodeus on 8/1/22, 4:33 PM
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?
by yccs27 on 8/1/22, 3:17 PM
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.
by agluszak on 8/1/22, 2:29 PM
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.
by benreesman on 8/1/22, 1:12 PM
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.
by yababa_y on 8/1/22, 11:44 AM
I love this walkthrough! It reproduces, in narrative form, the experience of interactive theorem proving. Great exploration of a niche detail.
by PoignardAzur on 8/1/22, 7:10 PM
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.
by mtlmtlmtlmtl on 8/1/22, 5:44 PM
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.
by siraben on 8/1/22, 4:35 PM
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.
```
by Tainnor on 8/1/22, 10:09 PM
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.
by mirekrusin on 8/1/22, 9:22 PM
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...
by Tainnor on 8/1/22, 4:51 PM
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.
by howling on 8/1/22, 2:29 PM
Personally, I find the title to be slightly misleading as the proof is essentially just (un)currying for dependently typed function.
by kelnos on 8/1/22, 9:56 PM
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`.
by max_ on 8/1/22, 5:00 PM
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?