Coding by guess and check
Karl Popper described science - I think convincingly - like this:
- A theory cannot be proven true, only disproven by experiment.
- Therefore, falsifiability is a critical feature of scientific theories. A theory needs to make predictions that could be proven false by observation.
- It follows that when testing a theory, focus on how you might prove it wrong.
- If you fail to disprove it, then you might tentatively accept the theory as the best explanation we have so far!
- And that acceptance will lead to more theories which we can then try to falsify.
He described this process as one of alternating cycles of “conjecture” (coming up with a theory) and “refutation” (attempting to falsify or criticise the theory).
I was introduced to this idea by David Deutsch’s book The Beginning of Infinity, where he uses the phrase “conjecture and criticism”, which alliterates nicely. I prefer the more colloquial “guess and check”.
I think this cycle also describes common practises involved in developing software.
- Writing the source code of, say, a sorting function is a conjecture: “I guess this source code correctly implements the quicksort algorithm”.
- Writing a test case is one way of “refuting”, “criticising”, or checking your conjectural source code. We usually supply “happy path” examples which, while not constituting “proof”, do provide some evidence. If these attempts to falsify your conjecture fail, you might be happy to proceed, depending on how complicated the original code is.
- Property-based testing is a way to automatically generate a lot of criticism, provided you have a way of judging the output. The properties themselves are further conjectures, for example of the form “I guess this source code checks that all elements of a list are smaller than their successor”. We depend on these properties being easier to state in code than the function they’re checking!
- Proofs and model checking approach the problem from a different direction. Additional conjectures such as “this proof correctly models the problem of sorting” or “this model accurately reflects the system I am building”, combined with “this source code corresponds accurately to this proof statement or model component” can be subject to their own criticism. A proof checker, itself correctly implemented, supplies criticism of a proof text.
I’ve described writing both the original code, and the tests or properties or proofs, as conjectural. In my view these approaches to the same underlying “explanation”, from different angles, buttress each other - acting as potential refutations of each other’s conjecture.
Different modes of expression - source code, examples, properties, proofs - give our minds different affordances to express and explain ourselves. Where these different expressions intersect and either agree or disagree, we get to understand the mistakes we made in each expression.
It’s by challenging ourselves that we can be more confident that our theories, our guesses, about what our code is doing. As Popper translated Xenophanes:
As for certain truth, no one has known it … and even if by chance he were to utter the perfect truth, he would himself not know it; for all is but a woven web of guesses.