Writing Code like a Mathematical Proof

Beginning in my early years of software development, I was interested in the way formal math shared similarities with writing code. In math, we learned about the concept of proofs, and how, starting from a set of axioms and definitions, one could logically construct true statements to prove a conjecture. Once proven, a conjecture becomes a theorem, and then it’s possible to use this theorem to prove other conjectures.

This line of solving proofs follows a similar set of steps in software development. We start off with a set of definitions (if statements, for loops, etc) and already proven theorems (standard libraries, third-party libraries, etc), then try to combine those elements to solve our own problems. The combination of statements in software is taken quite literally. Each line in computer code is evaluated as a logical sequence of instructions during a program run.

The following quote from an introductory textbook on mathematical analysis describes the comparison between writing proofs and essay writing. Steven Abbott, the author of Understanding Analysis, writes:

“[…]A proof is an essay of sorts. It is a set of carefully crafted directions, which, when followed, should leave the reader absolutely convinced of the truth of the proposition in question. To achieve this, the steps in a proof must follow logically from previous steps or be justified by some other agreed-upon set of facts. In addition to being valid, these steps must also fit coherently together to form a cogent argument”

This comparison between proof writing and essays forms the basis of my argument between proof writing and writing code. Before we begin, I want to point out that I will not be trying to convince the reader to mathematically prove their code à la Donald Knuth. Instead, I want to use the concepts of writing good proofs, and translate them to writing good code. This post covers a few of these similarities; providing an additional perspective when attempting to write quality code.

To ensure the consistency of a proof, let’s run through an example. Suppose we wanted to prove that the sum of two consecutive integers is always odd. As stated before, we’re looking to combine a sequence of logical statements, starting from definitions (or prior proven theorems), and build them up to a true result. Here’s what an example proof looks like:

Theorem

If a and b are consecutive integers, then the sum a + b is odd.

Proof

Assume that a and b are consecutive integers. By definition, an odd integer is written as 2k + 1 where k is any integer.

Because a and b are consecutive we know that b = a + 1.

Therefore, the sum a + b can be re-written as:

a + b = a + (a + 1) = a + a + 1 = 2a + 1

Since a is an integer, then 2a + 1 is odd, and therefore the sum a + b is odd.

Know your audience

Let’s break down some important parts about the proof, and some assumptions made about the audience. First, I assumed that readers of this post understood what an integer was (a safe assumption due to the nature of a programming post). Next, I assumed that readers would be comfortable with the algebra of integers (operations on integers are mostly intuitive). Finally, instead of assuming a reader knew the formal definition of odd integers, I defined it within the proof to ensure a consistent set of mental models between author and reader. With each assumption and definition declared, I built up to the final result using strictly true statements, and successfully proved the intended result.

Making required assumptions about your audience will always be a necessary step of formal proof writing. There are multiple ways of writing the example proof. One way would be to assume readers knew the formal definitions of even and odd integers. By dropping that definition, it makes the proof short and concise, but sacrifices explicitness. Instead, I figured the audience of this post may never have taken a pure math course before, or, if they had, would have forgotten the definition.

Good proof writers know who their target audience is. If they’re writing proofs for an introductory textbook, reminding readers of basic definitions will help ease them into the material. If they’re writing a journal article for a specific branch of mathematics, then they might discard definitions by rightfully assuming advanced mathematicians will be following along. Taking correct assumptions of the audience will lead to a better proof reading experience.

Like proof writing, we should make the same line of assumptions when writing software. When most developers write software, they are only trying to write executable code. Unfortunately, solely adhering to the necessity of executability does not guarantee code readability. Just because your code executes, does not mean it’s easy for someone to follow along the execution path. This works great when you’re trying to test your code, but not if you’re trying to maintain a long lasting team managed codebase.

To write understandable code, always ask the question of who your audience is. What level of experience do they have? What are the prerequisites they should know before reading this function? There are even differences in the semantics between programming languages, so knowing the best practices, and the language coding style, will ensure you are writing readable code for developers in that language.

When sitting down to write your next function, be mindful of the words you choose to describe your variables and methods. Take into account what assumptions you make, and how you structure your comments and code. Creating, or adhering to, a project style guide can also keep your code understandable for newcomers and veterans of a codebase. By following this principle, your code will not only read better, but it will reduce your fellow developer’s mental overhead when following along.

Write clearly and concisely

When writing code, we have modern conveniences to check the validity of statements in the form of compile errors, runtime exceptions, and automated unit tests. Writing proofs contain none of these conveniences. The mathematician’s answer checker is their fellow reader who must be convinced by the results of the proof. To convince the reader that the result is true, the proof writer must articulate it in the most clear and concise way. Struggling to grasp long, incoherent, and redundant statements leaves the reader frustrated and unable to make sense of the proof.

Because writing code is so often done in teams, we should be conscious of the reader. I propose we write our code in a way that not only executes the correct results, but convinces the reader the truth of the statements. Like a good proof, code should be written thoughtfully and carefully; we must make sure to cut redundant statements that offer no additional benefit to the reader.

Why take 100 lines of code to accomplish what could be done in 80, 60, or less? Dead code, like dead sentences, will tax the readers short term memory, forcing them to draw up a greater than required mind map. More often than not, your first stab at solving a problem will have taken the longest path of execution. Go back and try to edit what you have written, reducing its complexity of understanding.

Note, however, that I am not advocating to brush a generalized “reduce code” brush over your whole project. Taking this advice to the logical extreme will do more harm than good. There are times where instantiating a new, potentially redundant, variable may provide a better name to enhance the reader’s understanding.

Test all cases

Common tactics of solving a proof start from using one example, and then build up to a general statement. In our example proof, we can use the example of integers 2 and 3, and see that they will add up to 5 — an odd number. Using this example, we can extrapolate out and see how the pattern continues to apply.

We’re looking for a general solution, but that does not mean we can’t use practical examples to get us there. However, a problem can arise if we focus too much on practical examples. There are times we may forget to test a specific case which could break our general solution. In our example, we only looked at two positive integers. What about negative integers? How about using the integer’s additive identity (also known as 0)?

Luckily for the consecutive integers example, we won’t see an issue if we tried adding negatives or zero. Unfortunately, this won’t always be the case. Suppose we were trying to prove that each square root of an integer exists in the real numbers. If you tried √2, √4, or even √0, you would believe the result is true. However, there exists a problem if we try to find √-1, or the square root of any negative integer for that matter.

In fact, mathematicians had to create an entire new set of numbers — the complex numbers — to find square roots of negative integers! By incorporating a seemingly simple case of the negative integers, the history of mathematics changed forever. This is not even a rare example in math, there are countless times that mathematics has changed in face of a new requirement.

In software, we label the annoying, or unobvious, requirements as edge cases. Software developers have all encountered edge cases, especially when writing a function that takes in user input. It’s frustrating having to ensure that the function works for null data, too much data, or whatever insane inputs a user can come up with. Software engineers complain about edge cases all the time, and many neglect those edge cases causing their programs crash. While the naming for edge cases tries to label them as rare occurrences, they are still valid cases that must be accounted for.

I have come up with two reasons why software developers often neglect to test all cases:

1. They don’t know the case exists, or
2. They know the case exists, but don’t write the code that deals with it

The first point is a tricky one to solve, but like reviewers for proof writing, software developers have code reviews to double check their test cases. There are also ways to test your code using unit tests, integration tests, or model checkers like TLA+. We can also learn from experience to provide us with more knowledge on potential test cases. As you write more software, you’ll have encountered more cases, and this knowledge can be passed on to later implementations.

Going back to my two reasons, while the first point is an issue with ignorance, the second point is much more insidious. This occurs when a developer knows that an edge case can occur, but does nothing to guard against it. This is either due to project time restriction, rushing out a feature, or pure laziness. Each rationalization stems from the opportunity cost of putting additional time into a project, or shipping code with a known bug. Regardless of rationalization, this should never occur in our codebases.

Not only does it reflect poorly on the software you’ve built, it is logically wrong to neglect them. While I can sympathize with a developer realizing the additional burden of time when finding a new case, I cannot sit idly by while buggy code gets knowingly shipped. Like the mathematician who must create a whole new branch of mathematics by including negative integers, a great developer must take the time to build out edge case solutions in their code. Reframe these test cases from dealing with annoying edge cases, to building logically correct software that, like a proof, will stay strong in the face of any case.

In summary

I have done my best to find the three best mappings from great proof writing, to writing great software. While these three points do not exhaust all possible mappings, they are the ones that I have found the most useful when writing code. These two worlds are not that different, and you might be surprised that learning pure mathematics could help your ability to write better software in the future.

If these points were interesting to you, maybe you should crack open an elementary book on proofs and try your hand at a couple. Hopefully, like myself, you will find the same feeling when you solve your first proof from scratch: the familiar rush you get from writing correct code.