Philosophy

Author’s note: I wrote this in 2017 and it languished in the drafts since then because I couldn’t think of a good conclusion. Really this is typical of the subject matter and all this piece offers is something to chew on, if you have the interest in it or have never before considered the question. At the time I was helping tutor a TLA⁺ seminar and had the opportunity to ask Leslie Lamport (who has thought about computation quite a bit!) what he thought of the question with all his accumulated wisdom, and he replied “it’s one of those meaningless distinctions, like the difference between alive and not-alive.” So there you have it. Hopefully there are enough decent jokes in this post to make it worthwhile.

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.