Formal Methods and Me

My research isn't strictly in formal methods, or formal verification as it's sometimes called, but at some point I really found that I liked being a little extra careful with proofs. It started when I stumbled on Leslie Lamport's "How to Write a Proof", which talks about a way of structuring proofs in a way that encourages you to explain all the small steps. It is similar to the style of proofs introduced by David Hilbert. "How to Write a Proof" has several interesting stories about writing a proof, then trying to rewrite them in a structured proof format, and finding an error in the original proof as a consequence. As a programmer, it seemed like this was a great way to reduce errors in proofs.

So I tried it out, in my Analysis class. I took a proof from the book and created a structured version. It wasn't too bad since the proof was quite careful, but at one point I wondered "why did they use an open set here?" since the intuitive description of the proof didn't seem to need it. After a bit more thinking, I figured out that it was because they had to use a theorem described earlier in terms of open sets. And I don't think it mattered too much in that specific case, but at that moment I felt like I had a deeper understanding of what was going on, that I might have just skipped over once I got the intuition.

So then I got to thinking that in a program, a difference like this, between a function that does and doesn't use an open set, is an off-by-one error that often causes things to muck up. For more complicated programs, shouldn't we have tools that allow us to do this kind of reasoning in an automated way? This started my interest in formal methods, which at that point was mainly me trying to make structured proofs in my math courses. You would figure that mathematicians and programmers alike would love to find any way to reduce errors, but the resistance comes quite quickly.

There are horror stories of multipage proofs that 1+1=2, I think this one is actually true, but I don't know where it comes from. Mathematicians, I found, really like reading proofs as puzzles in themselves, this was also noted in "How to Write a Proof". Structuring the proof spoils the flowing prose, and detailing out the small steps in between is kind of like explaining a joke. Programmers have a similar feeling, though their concerns are usually over how much work is involved, or they will use the argument that "no proof or model can totally capture a system".

These concerns are somewhat justified, but for me, a nicely structured proof is just as nice as a nicely structured program, where the pieces fit together like parts of a puzzle. I think that is one good way to frame my view, some people might look at a jigsaw puzzle and say "ah, well there's a leaves here and there's the rest of the rest of the trunk, so these pieces must fit together", and indeed it is certainly true, but to me it's even better when you can actually see the pieces fit together.