Introduction
Once upon a time there were a bunch of brilliant (but weird) mathematicians who were involved in a cult. The cult was named the Cult of Pythagoras and existed in the 6th century BC in Ancient Greece. I could not find how many people were involved, but it was definitely larger than a handful of folks. They really liked numbers; believing that the truths of the universe were hidden in the purely rational number system. People thought of them to be like magicians and looked up to their wisdom. One day, their whole world was shattered by a man who tried to find the square root of two. It turns out that number is irrational, which went against everything these people believed. The Pythagoreans were so upset that they killed that man and threw his body into the ocean. Yikes.
I like math about 1.41421 percent as much as they did. Which is still a good amount! I like math because it helps me solve problems in a way that I can be confident is correct. When you build stuff, you need to know how things will work and fit together; else you can have a really hard time getting anything done. Think of a chair or a desk. You need four legs that are all the same height. How can you be confident your pieces are, in fact, of equal height? By measuring them of course! Maybe do a little bit of arithmetic to fit the situation so your measurements make sense. You are proving that the pieces are all the same height; that they will fit the position in which they belong, working as expected. This is the key idea of building things in a structured manner. The aforementioned cult brought about this manner of thinking that is prevalent in all of Western Philosophy. In this article we are going to apply the idea to software development, and hopefully you will understand how to think about code like a mathematician. To do this, we will try to learn how to frame blueprints in our mind, understand what it takes to prove something, and discuss what software tools are available in order to do our proofs.
Working From Blueprints
Let’s start from a practical side of things. Most work that one does in a professional setting will have some sort of guidelines to work off of. This is great, of course, because coming up with these guidelines is hard enough in of itself. To make the scope of this topic much more digestible, it will be assumed that the requirements already exist. These blueprints are your best friend, and it is your job to make them come to life. Normally that is not exactly an easy task, but we should be familiar with all of this so far. Building software products is no different; there are requirements and specifications that are expected to be followed. Agile methodologies can be used to manage these requirements and decide how to plan your work. One thing Agile cannot help you with is deciding how to do your work. Most engineers are skilled enough in problem solving to put pieces together and solve just about any problem. We are more concerned about how one can do work correctly that results in a sturdy product which is not easy to break.
Before we get into that, we will talk just a little more about blueprints. These blueprints are a list of qualities that the end product has. Another name for this is statements of truth. Imagine, how would a Pythagorean Cultist read the blueprints of a chair?
For any chair that claims to match this design, it must be true that each of its 4 legs are 2 feet long.
Chairs cannot make claims, but they do stand their ground (corny, I know). If I make a chair and claim that it fits the blueprint, I can easily measure the parts and prove this claim to be true. It is very important to think of things this way.
Claims and Proofs
Proving things is way easier than math class lead me to believe. We just need to think about what we are trying to prove. If it is the fact that the square root of two is irrational, then it is indeed a little hard. But let us start with proving that something is a number. Pick any number: let’s say 42. Done; that was easy and fun. Do we need to do more? 1729. 24. 10006660007. We get the gist, now we will break it down. We are claiming that there exists something that is a number. To prove this (or any statement) to be true, all we have to do is provide evidence. In this case just a number will suffice. Now I must admit, this proof is rather boring so let us move on to another one. I will now claim that 10006660007 is prime. I challenge the reader to write a program that proves this claim to be true or false. This should not be too hard, just divide our number by every number less than it (starting from 2) and if any divide neatly, then this number is not prime. When you are done, I will meet you in the next paragraph.
Hello from the next paragraph, did you solve it? All it takes to prove this is to provide evidence. A logically sound program that will report back true or false is definitely enough evidence. Spoiler: it is prime, and funny enough it is a beastial prime because of the 666 present in it. A lot of prime numbers have 666 in them which made Medieval mathematicians really think they were working with some nasty stuff. We are here to learn from their mistakes. Now, this probably is not your first proof. We humans do proofs all of the time. Ever look both ways when crossing the street? That is how you prove no cars are coming. Ever go outside to feel the weather? That is how you prove your weather app is correct.
I should note at this point, the nature of these proofs are purposely simple. We prove small and obvious facts to build up confident building blocks, and combine these truths together to solve more complicated problems (familiar?). You probably cannot prove a method to find out how many primes are less than any given number. If you could, you would be able to rule the world. That is probably too ambitious. Keep it simple and prove only what you need. On the “entire chair” level, how can you prove that your product matches the blueprints exactly? I have no clue; it would take way too much thinking. On the contrary, I can easily prove each piece is the right size and is in the proper position. With each piece being correct, there is no way for any uncertainty to work its way into our product.
I would not be a very good mathematician if I did not talk about the other types of proofs that we have available. So far, we have been talking about direct proofs. I give direct evidence that proves my claim. This is useful for the types of problems we have been discussing. Not all problems you will face can be solved using direct proofs, unfortunately. Another type is proof by contradiction (reductio ad absurdum). A claim is proved by contradiction when you show that the inverse is incorrect. The last type of proof for today is proof by induction. This is a fun one. To prove using induction, you need to prove a claim in the simplest case, then prove it will also work for the following case and all cases onward. Each proof method solves different types of problems, and often can be interchangeable based on how you frame the problem. Those who are not familiar with these topics are encouraged to do some of their own research.
Connection to Software
So now we know how to do basic proofs. We also have established that there are blueprints in software engineering that we work off of. Where does our proverbial software chair come into play? How can we “measure the legs” in code? Easy, let’s think of an example. Imagine you are given the requirements to write a server program that responds to all incoming messages that say “Ping” with “Pong”, but will not respond to any other type of message. After writing this program, you want to prove to a Medieval mathematician that it is correct. You can do this by simply providing evidence that is performs its specified duty. What type of proof should we use for this one? Let us use a combination of the direct and contradictory proof to really convince the mathematician, who would expect you to be really thorough. To start with the direct proof, it would be enough to show that the program does indeed respond “Pong” to incoming “Ping” messages. Now, to really be thorough, you have to think about the negative case. A correct program would not respond “Pong” to other messages. If you can show both of these cases are true for your program, even the staunchest mathematician would be convinced.
How do you actually do this with software and computers we have today? Well, those with a bit of experience would probably recognize that we can write tests. The art of testing is not something that I will dive into, as there are many resources out there for those interested. What is important to know is the way tests are phrased. Today, the testing framework will be Jest in Javascript. Let us start with an example.
describe( “the number 10006660007”, () => {
it( “is prime”, () => {
for ( let i = 2; i < 10006660007; i++ ) {
expect(10006660007 % 0).not.toBe(0);
}
}) it( “is beastial”, () => {
expect(“10006660007”.match(/666/)).toBeDefined()
}) /* … */
})
Breaking this down, we see some fun prose within this code. Describe the number 10006660007. It is prime. It is beastial. Doesn’t really leave any room for confusion, right? Clearly this is on purpose. These are the statements/claims that require proof. We put these proofs in the body of the tests. Note there are many ways to prove using code, but the pattern Jest uses is easy to grasp. Let’s phrase these tests in a way that a Medieval mathematician would understand.
If 10006660007 were to be prime, then it must be true that for every integer i between 2 and 10006660007, i is not a factor of 10006660007. If 10006660007 is beastial, then it must be true that 666 is present within the number.
When we run these tests, they will either pass or fail. We interpret a pass as a valid proof that our code has behavior/properties that we claim it has in the tests. At this point, we can now see our tests being a list of claims and proofs. Think back to blueprints being a list of requirements. Tests can match these as closely as needed. From there we can go to the moon with different romantic ways to think about programs. We will conclude with one of them.
Conclusion
Logic and programming is deeply rooted in mathematics. We are lucky to be around at the time when math is so decentralized and accessible to anyone with a computer. It is important to not lose the core fundamentals that many brilliant thinkers have laid out before us. I want the reader to part with a good beginning to thinking of programming as a dictionary of requirements and proofs. With the right kind of tests and planning, this becomes a very powerful and formal method for building products. Thanks for reading!
