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.
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).
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..
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.
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.
((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) is equivalent to (∀ x. (P(x) → Q)) ⇔ ((∃ x. P(x)) → Q)
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.
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.
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.
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.
What would you have titled the blog instead to be less misleading?
[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
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.
Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
firstorder.
Qed.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.
[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...