Formal-Methods

Note: this post was written for Lean 3; the latest version, Lean 4, is a very different language.

Turn back the clock to 2009: a confused physics major newly infatuated with math and computer science, I enrolled in MATH 273: Numbers and Proofs at the University of Calgary. This wasn’t my first encounter with mathematical proof; in first-year calculus I’d mastered rote regurgitation of delta-epsilon proofs. Despite writing out several dozen, their meaning never progressed beyond a sort of incantation I can summon to this day (for every \( \epsilon > 0 \) there exists a \( \delta > 0 \) such that…). We were told on the first day of MATH 273 that the purpose of proof is to compel belief. This was a bright start but sadly marked the beginning of a deeply embarrassing semester reaching its nadir when I asked the professor “how do we prove a definition” fully two-thirds of the way through the course. I got a B-.

Lessons I’ve learned from software engineering are uniformly cynical:

• Abstraction almost always fails; you can’t build something on top of a system without understanding how that system works.
• Bleeding-edge methods are a recipe for disaster
• Everything good is hype and you’ll only ever get a small fraction of the utility being promised.

Imagine my surprise, then, when the Z3 constraint solver from Microsoft Research effortlessly dispatched the thorniest technical problem I’ve been given in my short professional career.

Why are we here?

What guarantees does formal verification provide? This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all!

What do we mean by software correctness?

There are precisely two different ways for a piece of software to be correct:

• The supreme deity of the universe descends from the heavens and decrees, with all the weight of Objective Truth, that a certain piece of software is correct.
• We have a list of things we want the software to do, and use logic to prove the software does these things.

Crafty readers will come up with, like, twenty different caveats to the second definition. I encourage it! Take a minute to unearth some of the hidden assumptions. Good? Good. I’ll talk about those hidden assumptions in greater detail below, but the point I want to make is this: there is no such thing as inherently correct software. Your wacky program could say 1 * 1 = 2, and that isn’t incorrect in any objective sense - if that’s how you want your program to behave, heck, knock yourself out. We call our list of things we want the software to do a specification. A program is only correct (or incorrect) relative to its specification; if the program is correct relative to its specification, we say it implements or refines the specification.