Programming is more than coding

This is a translation article from the Stanford Workshop . But before her is a small introduction. How are zombies formed? Everyone fell into a situation where you want to pull a friend or colleague to your level, but it does not work out. Moreover, “it doesn’t work out” not so much with you as with him: on one side of the scales is a normal salary, tasks and so on, and on the other - the need to think. Thinking is unpleasant and painful. He gives up quickly and continues to write code, completely without including the brain. You imagine how much effort you need to spend to overcome the barrier of learned helplessness, and you just don’t do it. Thus, zombies are formed, which seem to be cured, but it seems that no one will do this.

When I saw that Leslie Lampport (yes, that same textbook comrade) was coming to Russiaand makes not a report, but a question-and-answer session, I was a little wary. Just in case, Leslie is a world-famous scientist, the author of fundamental works in distributed computing, and you can also know him by the letters La in LaTeX - “Lamport TeX”. The second alarming factor is his demand: everyone who comes should (completely free) listen in advance to a couple of his reports, come up with at least one question on them, and only then come. I decided to see what Lampport was broadcasting there - and it was great! This is exactly that thing, a magic link pill for treating a zombie. I warn you: from the text it can notably burn out for fans of super-flexible methodologies and non-enthusiasts to test what is written.

After habrokat, in fact, the translation of the seminar begins. Enjoy reading!

Whatever task you take, you always need to go through three steps:

• decide what goal you want to achieve;
• decide exactly how you will achieve your goal;
• come to your goal.

This also applies to programming. When we write the code, we need:

• decide what the program should do;
• determine exactly how it should fulfill its task;
• write the appropriate code.

The last step, of course, is very important, but I will not talk about it today. Instead, we discuss the first two. Each programmer performs them before starting to work. You do not sit down to write if you have not decided what you are writing: a browser or a database. A definite idea of ​​the goal must be present. And you are sure to think over what exactly the program will do, and not write it somehow in the hope that the code itself will somehow turn into a browser.

How exactly does this preliminary thinking of the code take place? How much effort should we spend on this? It all depends on how difficult the problem we are solving. Suppose we want to write a fault tolerant distributed system. In this case, we should consider everything properly before sitting down for the code. And if we just need to increase the integer variable by 1? At first glance, everything is trivial here, and no thoughts are needed, but then we recall that overflow may occur. Therefore, even in order to understand whether a problem is simple or complex, you first need to think.

If you think through possible solutions to the problem, you can avoid mistakes. But this requires that your thinking be clear. To achieve this, you need to write down your thoughts. I really like Dick Gindon's quote: “When you write, nature shows you how sloppy your thinking is.” If you do not write, it only seems to you that you are thinking. And you need to write down your thoughts in the form of specifications.

Specifications fulfill many functions, especially in large projects. But I will talk only about one of them: they help us to think clearly. Thinking clearly is very important and quite difficult, so here we need any help. What language should we write the specifications in? This is always always the first question for programmers: in what language we will write. There is no one correct answer to it: the problems that we solve are too diverse. TLA + is useful for some - this is the specification language that I developed. For others, it’s more convenient to use Chinese. It all depends on the situation.

Another question is more important: how to achieve clearer thinking? Answer: we must think like scientists. This is a way of thinking that has proven itself over the past 500 years. In science, we build mathematical models of reality. Astronomy was perhaps the first science in the strict sense of the word. In the mathematical model used in astronomy, celestial bodies appear as points with mass, position and momentum, although in reality they are extremely complex objects with mountains and oceans, tides. This model, like any other, is designed to solve certain problems. It is great for determining where to point the telescope, if you need to find a planet. But if you want to predict the weather on this planet, this model will not work.

Mathematics allows us to determine the properties of a model. And science shows how these properties relate to reality. Let's talk about our science, computer science. The reality with which we work is computing systems of various types: processors, game consoles, computers, executing programs, and so on. I will talk about running a program on a computer, but, by and large, all these conclusions apply to any computer system. In our science, we use many different models: a Turing machine, partially ordered sets of events, and many others.

What is a program? This is any code that you can consider yourself. Suppose we need to write a browser. We perform three tasks: we design the presentation of the program for the user, then we write a high-level scheme of the program, and finally we write the code. As we write the code, we understand that we need to write a tool for formatting the text. Here we again need to solve three problems: determine which text this tool will return; choose an algorithm for formatting; write code. This task has its own subtask: correctly insert a hyphen into words. We also solve this subtask in three steps - as we see, they are repeated at many levels.

Let us consider in more detail the first step: what problem the program solves. Here we most often model a program as a function that receives some input and gives some output. In mathematics, a function is usually described as an ordered set of pairs. For example, the squaring function for natural numbers is described as the set {<0,0>, <1,1>, <2,4>, <3,9>, ...}. The scope of such a function is the set of the first elements of each pair, that is, natural numbers. To define a function, we need to specify its scope and formula.

But functions in mathematics are not the same as functions in programming languages. Mathematics is much simpler. Since I don’t have time for complex examples, consider a simple one: a function in C or a static method in Java that returns the largest common divisor of two integers. In the specification of this method, we write: it computes GCD(M,N)for the arguments Mand N, where GCD(M,N)is a function whose domain is the set of pairs of integers, and the return value is the largest integer by Mand N. How does reality relate to this model? The model operates with integers, and in C or Java we have 32-bit int. This model allows us to decide whether the algorithm is correctGCDbut it will not prevent overflow errors. This would require a more complex model, for which there is no time.

Let's talk about the limitations of the function as a model. The work of some programs (for example, operating systems) does not boil down to returning a certain value for certain arguments; they can be executed continuously. In addition, the function as a model is poorly suited for the second step: planning a method for solving the problem. Quick sorting and bubble sorting compute the same function, but these are completely different algorithms. Therefore, to describe how to achieve the goal of the program, I use a different model, let's call it the standard behavioral model. The program in it is presented as the set of all permissible behaviors, each of which, in turn, is a sequence of states, and a state is an assignment of values ​​to variables.

Let's see what the second step for the Euclidean algorithm will look like. We need to calculate GCD(M, N). We initialize Mhow xand Nhow y, then repeatedly subtract the smaller of these variables from the larger, until they are equal. For example, if M = 12, a N = 18, we can describe the following behavior:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

And if M = 0and N = 0? Zero is divisible by all numbers, so there is no greatest divisor in this case. In this situation, we need to return to the first step and ask: do we really need to calculate the GCD for non-positive numbers? If this is not necessary, then you just need to change the specification.

A small digression about productivity should be made here. It is often measured by the number of lines of code written per day. But your work is much more useful if you get rid of a certain number of lines, because you have less space for bugs. And the easiest way to get rid of the code is in the first step. It is possible that you simply do not need all those bells and whistles that you are trying to implement. The fastest way to simplify a program and save time is to not do things that are not worth doing. The second step is in second place in terms of potential for saving time. If you measure productivity by the number of lines written, then thinking about how to complete the task will make you less productive., since you can solve the same problem with less code. I can’t give exact statistics here, because I have no way to calculate the number of lines that I did not write because I spent time on the specification, that is, on the first and second steps. And the experiment can not be put here either, because in the experiment we have no right to complete the first step, the task is predetermined.

In informal specifications, many difficulties are easily overlooked. There is nothing complicated in writing strict specifications for functions; I will not discuss this. Instead, we'll talk about writing strict specifications for standard behavioral models. There is a theorem that states that any set of behaviors can be described using the safety property and the liveness property.. Security means that nothing bad will happen, the program will not give the wrong answer. Vitality means that sooner or later something good will happen, that is, the program will sooner or later give the correct answer. As a rule, security is a more important indicator; errors most often arise here. Therefore, to save time, I will not talk about survivability, although it, of course, is also important.

We achieve security by prescribing, firstly, the many possible initial states. And secondly, relationships with all possible next states for each state. We will behave as scientists and define the states mathematically. A set of initial conditions is described by, for example, in the case of the Euclidean algorithm: (x = M) ∧ (y = N). For certain values Mand Nthere is only one initial state. The relationship with the next state is described by a formula in which the variables of the next state are written with a stroke, and the current state without a stroke. In the case of the Euclidean algorithm, we will deal with the disjunction of two formulas, in one of which xis the largest value, and in the second - y:

In the first case, the new value of y is equal to the previous value of y, and we get the new value of x, subtracting the smaller from the larger variable. In the second case, we do the opposite.

Let's get back to the Euclidean algorithm. Suppose again that M = 12, N = 18. It defines a single initial state (x = 12) ∧ (y = 18). Then we substitute these values ​​in the formula above and get:

Here, the only possible solution: x' = 18 - 12 ∧ y' = 12and we get behavior: [x = 12, y = 18]. Similarly, we can describe all the states in our behavior: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

In the last state, [x = 6, y = 6]both parts of the expression will be false, therefore, he has no next state. So, we have a full specification of the second step - as we see, this is quite ordinary mathematics, like that of engineers and scientists, and not strange, like in computer science.

These two formulas can be combined into one formula of temporal logic. She is elegant and easy to explain, but now she has no time. Temporal logic we may need only for the property of liveliness, for security it is not needed. Temporal logic as such is not pleasant, it is not quite ordinary mathematics, but in the case of liveliness it is a necessary evil.

In Euclid's algorithm for each value xand yit has a unique value x', and y'that makes the relationship with the following condition is true. In other words, the Euclidean algorithm is deterministic. In order to simulate a non-deterministic algorithm, it is necessary that the current state has several possible future states, and that each value of the variable without a prime has several values ​​of the variable with a stroke at which the relation with the next state is true. This is not difficult to do, but I will not give examples now.

To make a working tool, you need formal math. How to make the specification formal? To do this, we need a formal language, for example, TLA + . The specification of the Euclidean algorithm in this language will look like this:

The equal sign symbol with a triangle means that the value to the left of the sign is defined as equal to the value to the right of the sign. In essence, a specification is a definition, in our case, two definitions. You need to add declarations and some syntax to the specification in TLA +, as in the slide above. In ASCII, it will look like this:

As you can see, nothing complicated. The specification for TLA + can be checked, i.e., bypass all possible behaviors in a small model. In our case, this model will be certain values ​​of Mand N. This is a very efficient and easy verification method that runs entirely automatically. In addition, you can write formal proofs of the truth and verify them mechanically, but this takes a lot of time, so almost no one does it.

The main disadvantage of TLA + is that it is mathematics, and programmers and computer scientists are afraid of mathematics. At first glance, this sounds like a joke, but, unfortunately, I say this in all seriousness. My colleague just told me how he tried to explain TLA + to several developers. As soon as the formulas appeared on the screen, they immediately had glass eyes. So if TLA + is scary, you can use PlusCalIt is a kind of toy programming language. An expression in PlusCal can be any TLA + expression, that is, by and large, any mathematical expression. PlusCal also has syntax for non-deterministic algorithms. Due to the fact that any TLA + expression can be written in PlusCal, it is much more expressive of any real programming language. Next, PlusCal compiles into the easy-to-read TLA + specification. This does not mean, of course, that the complex PlusCal specification will turn into a simple one on TLA + - just the correspondence between them is obvious, there will be no additional complexity. Finally, this specification can be verified with TLA + tools. In general, PlusCal can help overcome the phobia of mathematics; it is easy to understand even for programmers and computer scientists.

Perhaps someone will object that TLA + and PlusCal are mathematics, and mathematics works only on invented examples. In practice, you need a real language with types, procedures, objects, and so on. This is not true. Here is what Chris Newcomb, who worked at Amazon, writes: “We used TLA + in ten large projects, and in each case, its use made a significant contribution to the development, because we were able to catch dangerous bugs before getting into production, and because he gave us understanding and confidence necessary for aggressive performance optimizations that do not affect the truth of the program ”. You can often hear that when using formal methods we get an inefficient code - in practice, everything is exactly the opposite. In addition, it is believed that managers cannot be convinced of the need for formal methods, even if programmers are convinced of their usefulness. And Newcomb writes: “Managers are now pushing in every way to write specifications on TLA +, and they specially devote time for this”. So when managers see that TLA + is working, they are happy to accept it. Chris Newcomb wrote this about six months ago (in October 2014), now, as far as I know, TLA + is used in 14 projects, not 10. Another example relates to the design of the XBox 360. An intern came to Charles Thacker and wrote specification for a memory system. Thanks to this specification, a bug was found that otherwise would not have been noticed, and because of which each XBox 360 would fall after four hours of use. IBM engineers have confirmed that their tests would not have detected this bug.

You can read more about TLA + on the Internet, and now let's talk about informal specifications. We rarely have to write programs that compute the least common divisor and the like. More often, we write programs like the pretty-printer tool I wrote for TLA +. After the simplest processing, the TLA + code would look like this:

But in the above example, the user most likely wanted the conjunction and equal signs to be aligned. So the correct formatting would look more like this:

Consider another example:

Here, on the contrary, the alignment of equal signs, addition and multiplication in the source was random, so the simplest processing is enough. In general, there is no exact mathematical definition of the correct formatting, because “correct” in this case means “what the user wants”, and this cannot be mathematically determined.

It would seem that if we do not have a definition of truth, then the specification is useless. But this is not so. If we don’t know what exactly the program should do, this does not mean that we do not need to think through its work - on the contrary, we should spend even more effort on this. The specification here is especially important. It is impossible to determine the optimal program for structural listing, but this does not mean that we should not undertake it at all, and writing code as a stream of consciousness is not a thing. In the end, I wrote a specification of six rules with definitions in the form of comments in a Java file. Here is an example of one of the rules: a left-comment token is LeftComment aligned with its covering token. It is usually written in, say, mathematics English: LeftComment aligned, left-commentandcovering token- terms with definitions. This is how mathematicians describe mathematics: write definitions of terms and based on them - rules. The benefit of this specification is that understanding and debugging the six rules is much simpler than 850 lines of code. I must say that writing these rules was not easy, quite a lot of time was spent on debugging them. Especially for this purpose, I wrote code that reported which rule was used. Due to the fact that I checked these six rules with a few examples, I did not need to debug 850 lines of code, and the bugs turned out to be quite easy to find. Java has some great tools for this. If I just wrote the code, it would take me much longer, and the formatting would turn out to be of worse quality.

Why was it impossible to use a formal specification? On the one hand, the correct execution is not very important here. A structural listing is sure to not please anyone, so I did not need to get the right work in all unusual situations. Even more important is the fact that I did not have adequate tools. The tool for checking TLA + models is useless here, so I would have to manually write examples.

The specification given has features common to all specifications. It is of a higher level than code. You can implement it in any language. To write it, any tools or methods are useless. No programming course will help you write this specification. And there are no tools that could make this specification unnecessary unless, of course, you write a language specifically for writing structural listing programs on TLA +. Finally, this specification says nothing about exactly how we will write the code, it only indicates what this code does. We are writing a specification to help us think through the problem before we start thinking about code.

But this specification also has features that distinguish it from other specifications. 95% of other specifications are much shorter and simpler:

Further, this specification is a set of rules. This is usually a sign of poor specification. Understanding the implications of the ruleset is quite difficult, which is why I had to spend a lot of time debugging them. However, in this case I could not find a better way.

It is worth saying a few words about programs that work continuously. As a rule, they work in parallel, for example, operating systems or distributed systems. Very few can understand them in their minds or on paper, and I am not one of them, although I once could afford it. Therefore, tools are needed that will test our work - for example, TLA + or PlusCal.

Why did you need to write a specification if I already knew what exactly the code should do? In fact, it only seemed to me that I knew it. In addition, if there is a specification, an outsider no longer needs to get into the code to understand what exactly he is doing. I have a rule: there should not be any general rules. This rule, of course, has an exception, this is the only general rule that I follow: the specification of what the code does is to tell people everything they need to know when using this code.

So what exactly do programmers need to know about thinking? For starters, the same as everyone: if you do not write, then you only think that you are thinking. In addition, you need to think before coding, which means you need to write before coding. A specification is what we write before we start coding. The specification is needed for any code that can be used or modified by anyone. And this “someone” may turn out to be the author of the code a month after writing it. The specification is needed for large programs and systems, for classes, for methods, and sometimes even for complex sections of a single method. What exactly needs to be written about the code? It is necessary to describe what he is doing, that is, what can be useful to any person using this code. Sometimes it may also be necessary to indicate exactly how the code achieves its goal. If we passed this method in the course of algorithms, then we call it an algorithm. If it is something more special and new, then we call it high-level design. There is no formal difference: both are an abstract model of the program.

How exactly should a code specification be written? The main thing: it should be one level higher than the code itself. It should describe states and behaviors. It should be as strict as the task requires. If you write a specification of how to implement the task, then it can be written in pseudo-code or using PlusCal. Learning to write specifications is necessary on formal specifications. This will give you the necessary skills that will help including those with informal ones. How to learn to write formal specifications? When we learned programming, we wrote programs and then debugged them. The same thing here: you need to write a specification, check it using the model checking tool and fix errors. TLA + may not be the best language for a formal specification, and another language would probably be better for your specific needs.

How to link specification and code? With the help of comments that connect mathematical concepts and their implementation. If you work with graphs, then at the program level you will have arrays of nodes and arrays of links. Therefore, you need to write exactly how the graph is implemented by these programming structures.

It should be noted that none of the above applies to the process of writing code. When you write code, that is, perform the third step, you also need to think and think through the program. If a subtask is difficult or not obvious, you need to write a specification for it. But I am not talking about the code itself. You can use any programming language, any methodology, it's not about them. In addition, none of the above eliminates the need to test and debug code. Even if the abstract model is written correctly, there may be bugs in its implementation.

Writing specifications is an additional step in the process of writing code. Thanks to him, many errors can be caught with less effort - we know this from the experience of programmers from Amazon. With specifications, the quality of the programs becomes higher. So why then do we do without them so often? Because writing is hard. And it’s hard to write, because you need to think for this, and thinking is also difficult. It’s always easier to pretend what you think. Here you can draw an analogy with running - the less you run, the slower you run. You need to train your muscles and exercise in writing. Need practice.

The specification may be incorrect. You could have made a mistake somewhere, or your requirements may have changed, or it turned out you need to make an improvement. Any code that anyone uses has to be changed, so sooner or later the specification will no longer correspond to the program. Ideally, in this case, you need to write a new specification and completely rewrite the code. We know perfectly well that no one does this. In practice, we patch the code and possibly update the specification. If this is necessarily happening sooner or later, then why write specifications at all? Firstly, for the person who will rule your code, every extra word in the specification will be worth its weight in gold, and you yourself may well be that person. I often scold myself for insufficient specification when I edit my code. And I write more specifications than code. So when you edit the code, The specification always needs to be updated. Secondly, with each edit, the code gets worse, it becomes increasingly difficult to read and maintain. This is an increase in entropy. But if you do not start with the specification, then each written line will be a revision, and the code from the very beginning will be cumbersome and difficult to read.

As Eisenhower said , not a single battle was won according to plan, and not one battle was won without a plan . And he knew something about the battles. There is an opinion that writing specifications is a waste of time. Sometimes this is true, and the task is so simple that there is nothing to think over. But you should always remember that when you are advised not to write specifications, it means you are advised not to think. And every time you should think about it. Thinking through a task does not guarantee that you will not make mistakes. As we know, nobody invented the magic wand, and programming is a difficult task. But if you do not think over the task, you are guaranteed to make mistakes.

More information about TLA + and PlusCal can be found on a special site, you can go there from my home page using the link . That's all for me, thank you for your attention.

I remind you that this is a translation. When you write comments, remember that the author will not read them. If you really want to talk with the author, then he will be at the Hydra 2019 conference, which will be held on July 11-12, 2019 in St. Petersburg. Tickets can be purchased on the official website .