9 ms·

Formally Verifying Rust's Opaque Types

133 points by BreakfastB0b 4y ago

yababa_y 4y ago
I love this walkthrough! It reproduces, in narrative form, the experience of interactive theorem proving. Great exploration of a niche detail.
- BreakfastB0b 4y ago
  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.
  - vlovich123 4y ago
    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).
    - BreakfastB0b 4y ago
      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.
      - tatref 4y ago
        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`
        brabel 4y ago
        Without a trait bound that demands cloneable items, no.
    - themulticaster 4y ago
      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 https://isabelle.in.tum.de/overview.html [2] https://www.isa-afp.org/ https://www.isa-afp.org/
      - vlovich123 4y ago
        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.
  - dist1ll 4y ago
    > 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..
    - BreakfastB0b 4y ago
      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!
  - ratmice 4y ago
    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/ae54d9b27f7afa8cabb7cc84c42550e0 https://gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c425... couldn't get the link to work in the lean-web-editor though.
benreesman 4y ago
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 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.
stepchowfun 4y ago
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/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... [2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560cd55ed9b1e989947e99dcd6/proofs/Tactics.v#L81 https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
- irsagent 4y ago
  Could TLA+ do the same thing?
agluszak 4y ago
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.
- BreakfastB0b 4y ago
  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?
  - agluszak 4y ago
    Introduction to Coq theorem proving using Rust static dispatch equivalency example
howling 4y ago
Personally, I find the title to be slightly misleading as the proof is essentially just (un)currying for dependently typed function.
- BreakfastB0b 4y ago
  I’m not sure I understand the connection to dependent types, would you be able to elaborate?
  - howling 4y ago
    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).
    - BreakfastB0b 4y ago
      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.
yccs27 4y ago
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.
ArrayBoundCheck 4y ago
- throwaway17_17 4y ago
  Can you explain you explain your comments implied link between this blog post and what about Rust makes it not a ‘proper language’? Also, is it just the hype, community, etc that you don’t like about Rust or is it something else?
  - ArrayBoundCheck 4y ago
    Look at my username. I didn't like it since rust called themself memory safe and didn't force us to do an array bounds check. It's been 10years and they still haven't done it (Also all the hype and fearlessness is obnoxious)
    - throwaway17_17 4y ago
      I was under the impression that unless inside an unsafe block, Rust required/automatically-placed bounds checks on array accesses. The out there was for situations where the compiler could 'prove' that the index was within bounds statically. But maybe I was wrong about that. With such a strong focus on bounds checking, are there any 'systems programming' languages that you do find acceptable?
      - ArrayBoundCheck 4y ago
        > automatically-placed bounds checks on array accesses That's exactly why I get annoyed. How will it be fast if it branches on every access > where the compiler could 'prove' The compiler doesn't prove shit. It lets the optimizer do it. It's extremely easy to fool the optimizer > there any 'systems programming' languages The ones that don't make false claims (so not v or rust) and don't insert code I don't want
        throwaway17_17 4y ago
homodeus 4y ago
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?
siraben 4y ago
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.
Tainnor 4y ago
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.
max_ 4y ago
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?
mtlmtlmtlmtl 4y ago
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.
- tialaramex 4y ago
  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/ 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.
  - mtlmtlmtlmtl 4y ago
PoignardAzur 4y ago
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.
- throwaway17_17 4y ago
  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)
- Arnavion 4y ago
  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.
mirekrusin 4y ago
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-I4XROIJhkIU https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b... [1] https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk... [2] https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.html https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.h...
kelnos 4y ago
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`.
Tainnor 4y ago
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.

133 points by BreakfastB0b 4y ago

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

BreakfastB0b 4y ago
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.
- vlovich123 4y ago
  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).
  - BreakfastB0b 4y ago
    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.
    - tatref 4y ago
      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`
      - brabel 4y ago
        Without a trait bound that demands cloneable items, no.
  - themulticaster 4y ago
    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 https://isabelle.in.tum.de/overview.html [2] https://www.isa-afp.org/ https://www.isa-afp.org/
    - vlovich123 4y ago
      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.
- dist1ll 4y ago
  > 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..
  - BreakfastB0b 4y ago
    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!
- ratmice 4y ago
  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/ae54d9b27f7afa8cabb7cc84c42550e0 https://gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c425... couldn't get the link to work in the lean-web-editor though.

benreesman 4y ago

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 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.

stepchowfun 4y ago

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/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... [2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560cd55ed9b1e989947e99dcd6/proofs/Tactics.v#L81 https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

irsagent 4y ago
Could TLA+ do the same thing?

agluszak 4y ago

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.

BreakfastB0b 4y ago
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?
- agluszak 4y ago
  Introduction to Coq theorem proving using Rust static dispatch equivalency example

howling 4y ago

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

BreakfastB0b 4y ago
I’m not sure I understand the connection to dependent types, would you be able to elaborate?
- howling 4y ago
  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).
  - BreakfastB0b 4y ago
    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.

yccs27 4y ago

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.

ArrayBoundCheck 4y ago

throwaway17_17 4y ago
Can you explain you explain your comments implied link between this blog post and what about Rust makes it not a ‘proper language’? Also, is it just the hype, community, etc that you don’t like about Rust or is it something else?
- ArrayBoundCheck 4y ago
  Look at my username. I didn't like it since rust called themself memory safe and didn't force us to do an array bounds check. It's been 10years and they still haven't done it (Also all the hype and fearlessness is obnoxious)
  - throwaway17_17 4y ago
    I was under the impression that unless inside an unsafe block, Rust required/automatically-placed bounds checks on array accesses. The out there was for situations where the compiler could 'prove' that the index was within bounds statically. But maybe I was wrong about that. With such a strong focus on bounds checking, are there any 'systems programming' languages that you do find acceptable?
    - ArrayBoundCheck 4y ago
      > automatically-placed bounds checks on array accesses That's exactly why I get annoyed. How will it be fast if it branches on every access > where the compiler could 'prove' The compiler doesn't prove shit. It lets the optimizer do it. It's extremely easy to fool the optimizer > there any 'systems programming' languages The ones that don't make false claims (so not v or rust) and don't insert code I don't want
      - throwaway17_17 4y ago

homodeus 4y ago

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?

siraben 4y ago

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.

Tainnor 4y ago

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.

max_ 4y ago

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?

mtlmtlmtlmtl 4y ago

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.

tialaramex 4y ago
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/ 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.
- mtlmtlmtlmtl 4y ago

PoignardAzur 4y ago

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.

throwaway17_17 4y ago
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)
Arnavion 4y ago
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.

mirekrusin 4y ago

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-I4XROIJhkIU https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b... [1] https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk... [2] https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.html https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.h...

kelnos 4y ago

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`.

Tainnor 4y ago

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.