Type Theory & Reasoning About Code
I've remarked before that I believe testing to be a poor substitute for reasoning when it comes to code. In the time since that first post, I've come to believe this more & more firmly, as well as coming to find authoring (or, more recently, generating) suites of unit tests that meet some arbitrary threshold for code coverage to be increasingly tedious. Intuitively, I understood that leveraging the type system to make illegal program state unrepresentable was the way forward, but I was missing that which could stand-in for the unit test suite.
My search for that replacement led me to Coq. Coq is an interactive proof assistant. That means one uses it to prove theorems, and (as distinct from automated theorem provers) the system will help you to construct your proof interactively. Coq can & has been used to prove many things, such as the Four Color Theorem, but I'm more interested in proving propositions about programs.
Coq seemed promising to me: it allows one to develop code within the system, prove certain properties about it, and then extract the code to other languages more commonly used in industry. With that power, however, comes complexity. In the forward to "Interactive Theorem Proving and Program Development" the authors wish readers "good luck in their discovery of a difficult but exciting world".
Different people learn in different ways. Many, especially in the software industry, like to learn in a "bottom-up" manner: authors begin with a "Hello, world!" example (or whatever sort of example would be considered minimal by their intended audience) and build from there. I've always preferred to learn "top-down": what is the thing about which I'm learning and where does it fit into the things about which I already know? What are its principles and how can I reason for myself from those principles to the specific thing that I want to do?
Coq's advocates point out that verifying proofs in the system amounts to type checking; a proof is verified if it "type checks", and this is a well-understood & relatively straightforward process. This mystified me, and so I began learning about Type Theory. As an exercise in the Feynman technique, I'm going to try to solidify & consolidate my understanding by explaining it here. The first time I posted about this, I said that I hoped that that post would be the first in a series. It's been a while, but I'm finally picking that up now.
If you're interested in Coq, and you learn in what I called the "bottom-up" style, I highly recommend "Logical Foundations" by Benjamin Pierce, or "Certified Programming with Dependent Types" by Adam Chlipala. For myself, since Coq is at the end of the day a system for writing down valid terms in a certain formal language, my path was to understand that language beginning with whence it came. For that, we need to go back to start: Alonzo Church's λ Calculus, which is the subject of my next post.
Finally, I am very much an amateur here: when readers notice errors or omissions, corrections will be gratefully accepted.
05/14/24 16:55