Writing Code as a Mathematical Proof

The debate about whether a programmer needs mathematics or not will probably never subside. There are a million opinions for and against, but today we will not talk about that at all. We bring to your attention an adapted translation of the material by Spiro Sideris, in which he discusses how you can write program code, following the logic of mathematical proofs. When I started programming, I was always interested in considering the relationship between formal mathematics and the process of writing code. From mathematics, we learned how to build proofs, that is, how, based on a set of axioms and definitions, one can logically construct true statements in order to prove a certain hypothesis. Once proven, a hypothesis becomes a theorem and can be used to prove other hypotheses. Such a chain of proofs and transformations from hypotheses to theorems is somewhat similar to the sequence of steps in software development. We start with a lot of definitions (conditional statements, loops, and so on) as well as previously proven theorems (standard libraries, third-party libraries, and so on). Then we try to combine these elements to solve our problems. The combination of statements in software is done literally. Each line of computer code is evaluated as a logical sequence of instructions while the program is running. The following quote from a textbook on fundamentals of calculus describes a comparison between writing proofs and writing essays. Stephen Abbott, author of Understanding Analysis, writes: It is this comparison of proof building and essay writing that underpins my notion of the analogy between proof writing and writing code. Before we get started, I want to make it clear that I'm not trying to convince the reader to "mathematize" the code in the vein of Donald Knuth. I just want to use good proof building concepts to write quality code. In this article, I will describe several useful examples of proofs, the analysis of which, perhaps, will help improve the program code. Let's consider one of them. Suppose we need to prove that the sum of two consecutive integers is always odd. As stated earlier, we will seek to combine a sequence of logical statements, starting with definitions or previously proven theorems, to obtain our proof. Consider an example. Theorem If a and b are consecutive integers, then their sum (a + b) is always an odd integer. Proof Suppose a and b are consecutive integers. By definition, an odd number is written as 2k+1 , where k is any integer. Because aand bare consecutive numbers, we can write: b=a+1 . So their sum (a + b) can be written as:

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

Since a is an integer, therefore 2a+1 is an odd number. Thus, the sum (a + b) = 2a+1 is an odd number. Q.E.D.

Know your target audience

Let's go through some important parts of our proof and some assumptions about you, the readers of this material. First, I assumed that the readers of this article understand what integers are (due to the fact that we are talking about programming). Second, I suggested that readers would be comfortable working with integer algebra (because operations on integers are often intuitive). But, instead of assuming that the reader knows the formal definition of odd integers, I have included the definition along with the proof to ensure a consistent set of concepts between author and readers. With each subsequent assumption and definition, I created a proof using strictly true statements and successfully proved the theorem. Making the necessary assumptions about the audience level will always be a necessary step when writing a formal proof, as this can be done in many different ways. For example, if we assume that readers initially knew the formal definitions of even and odd numbers, I could not give them in the text, and then the proof would look very short. Instead, I assumed that one of my readers didn't take math class, or it was so long ago, that he had already forgotten all the definitions. A good author, whether it is writing a mathematical proof or an action-packed novel, must always understand for whom he writes, what kind of people will be his target audience. If we are talking about a textbook on the basics of mathematics for elementary school, then the material will be easier to perceive if the main definitions are indicated in it. If we are talking about an article in a specialized mathematical journal, the author, of course, can omit elementary definitions, rightly believing that his target audience are specialists in this field. Understanding the target audience will help to correctly formulate the evidence and convey it to readers. We can build a similar schema not only when writing proofs, but also when writing software. When most developers write a program, they mostly try to write executable code. However, if the code is executed, this does not guarantee its readability and understandability. Most likely, you will perfectly understand your own (or someone else's) little program. But what if you have to deal with tons of someone else's code in a million lines? To write understandable code, always ask a question about who your target audience is. What is their level of training? What basic knowledge they need to have in order to read the function you wrote. if you have to deal with tons of someone else's code in a million lines? To write understandable code, always ask a question about who your target audience is. What is their level of training? What basic knowledge they need to have in order to read the function you wrote. if you have to deal with tons of someone else's code in a million lines? To write understandable code, always ask a question about who your target audience is. What is their level of training? What basic knowledge they need to have in order to read the function you wrote. In addition, there are differences in semantics between programming languages, so knowing the best practices and styles of programming languages ​​will ensure that your code is easily readable by developers who specialize in that programming language. When you're about to write your next function, be mindful of the words you use to describe your variables and methods. For example, if you name a variable minimum to denote the minimum boundary of some set, most people will understand what you mean. But when used for the same variable, a more specific, albeit correct, infimum, either mathematicians or those who have recently studied the beginnings of analysis will understand you. Pay attention to how you structure your comments and code. Creating a style guide for a project, or following an existing style guide, will also help make your code easier for both juniors and experienced developers to understand. If you follow this principle, your code will be easy to read and will reduce the effort of your followers who will also understand your code.

Write clearly and concisely

Today, while writing code, we have the opportunity to check the code using the tools built into the IDE and text editors. In case of a violation of validity, a good IDE will give us a compilation error or a runtime exception . The construction of proofs, alas, does not involve such checks. The reader or student will check the mathematician's proof for validity. To convince the reader of the correctness of the result obtained, the author of the proof must formulate it in the most understandable and concise way. Long and incoherent reflections on the essence of being will not be able to convey to the reader the meaning of the proof. I suggest writing code in such a way that it is not only executable, but also transparent - convincing the reader of the truth of the statements. Like a good proof, the code must be written carefully and carefully. We must necessarily cut down on redundant data that does not give the reader additional benefit, but only confuses him. Why write a hundred lines of code when eighty, sixty, or even less is enough to complete the task? Dead code, like dead phrases, is too stressful for the reader. Most often, the solution to the problem will take a lot of time and effort. Go back and try to edit what you wrote to make it easier to understand. That being said, I am not advocating that you "reduce the amount of code" in the entire project. Extremes are not appropriate, and in this case they will also do more harm than good. Sometimes the creation of a new

Check all options

Very often, the proof of hypotheses begins with the use of a particular example, and then there is a transfer to the general case. In the above sequential number theorem, we can take two consecutive integers 2 and 3 for verification, indeed, their sum 5 is an odd number. Using this example, we can extrapolate and see how this pattern is applied further. Of course, we are looking for a general solution, but this does not mean that we cannot use practical examples to obtain the desired result. However, by focusing only on practical examples, we can make a mistake. Sometimes we may forget to check for a specific case that violates the general solution. In our example, we considered two positive integers. But what about negative numbers? What happens if we use a neutral element (in the case ofinteger , is it 0 )? Fortunately, in this particular example, the proof remains valid for negative numbers as well as for the neutral element. Unfortunately, this is not always the case. A simple school example. Suppose we need to prove that every square root of an integer exists in the real numbers. If you tried to take √2, √4 or even √0 as an example, then you think that the result is correct. However, what happens if we try to find the square root of any negative number? In fact, mathematicians had to create a whole new set of numbers—complex numbers—in order to find the square roots of negative integers. By including the seemingly simple variant of negative numbers, the history of mathematics changed. And this is far from the only case where mathematics has expanded to meet new requirements. In software, we classify variants in which the program works differently into a group of special cases and call them edge cases.(edge ​​cases). Software developers run into these edge cases regularly, especially when writing a function that accepts user input: you need to make sure it works if the user hasn't entered data, or has entered too much, or the data isn't as expected... The imagination of other users is limitless. . Software engineers regularly complain about edge cases, and many of them neglect them, causing programs to crash. Although we try to label edge cases as "rare" when naming them, in practice they are not that rare and should be taken into account. Developers don't always handle edge cases in their proposals, and here's why:

1. They left out the edge case because they don't know that such an option is possible;
2. They know that such an option is possible, but they do not write code that interacts with it.

The first point refers to a number of intractable problems. However, just as mathematicians have proof reviewers, developers have a code review (code review, in Russian-speaking countries they usually say so - code review) to check test cases. There are ways to test code with unit tests, integration tests, or model validation, such as TLA+. In addition, personal experience often helps us to find out in advance additional information about potential test options. The more programs you write, the more often you will have to deal with such cases, and your knowledge can be used in later developments. Returning to our two reasons, I note that if the first point is a problem of ignorance, then the second is much more insidious. This happens if the developer is aware of the possibility of an edge case, but does not try to figure out options for protecting against it. This can either be due to project time constraints, rush or sheer laziness. Every attempt at rationalization comes with the need to increase the amount of time to work on a project or piece of code with an error. Which, in principle, should not be in other cases. Little of, that it reflects badly on the software you create, it is logically wrong to ignore such cases. And while I understand the feelings of a developer who needs to spend extra time looking for a new problem, I believe that one cannot sit back until the problem is resolved. If a developer creates tests that take edge cases into account, he will end up with strong code that will work cleanly, like a true proof of a mathematical theorem.

Summing up

In this article, I tried to find the three most appropriate correspondences between writing mathematical proofs and writing program code. Of course, these three options are not the only ones, but I think they are the most useful for writing a program. The world of mathematics and the world of programming are much closer together than most people realize. And learning math can help you code better in the future. If the topic of this article seemed interesting to you, it might be worth trying to open a simple book on proofs and go through it. I hope that the pleasure of a theorem proven from scratch, for you, as well as for me, will be comparable to the pleasure of writing a good program.