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