This is a translated article . But before that, a brief introduction. How do zombies form? Everyone has found themselves in a situation where they want to elevate a friend or colleague to their level, but it doesn’t work. And the reason is not so much you, but them: on one side is a normal salary, tasks, and so on, while on the other is the necessity to think. Thinking is unpleasant and painful. They quickly give up and continue to write code without engaging their brain at all. Can you imagine how much effort it takes to overcome the barrier of learned helplessness, and they simply don't do it? This is how zombies are formed, who seemingly can be cured, but seemingly no one wants to take on that task.
When I saw that (yes, that same person from the textbooks) and was doing not a lecture, but a Q&A session, I was a bit cautious. Just in case, Leslie is a world-renowned scholar, author of foundational works in distributed computing, and you might also know him from the letters La in LaTeX—'Lamport TeX'. The second alarming factor is his requirement: anyone who comes must (completely for free) listen to a couple of his lectures in advance, come up with at least one question about them, and only then attend. I decided to see what Lamport was talking about—and it’s magnificent! It's exactly that thing, a magical link-tablet for curing zombification. Be warned: the text might ruffle the feathers of lovers of ultra-flexible methodologies and those who dislike testing their output.
After the hubbub, the actual seminar translation begins. Enjoy reading!
Whatever task you take on, you always need to go through three steps:
- determine what goal you want to achieve;
- decide how you will achieve your goal;
- reach your goal.
This also applies to programming. When we write code, we need to:
- decide what exactly the program should do;
- determine how exactly it should perform its task;
- write the corresponding code.
The final step is, of course, very important, but I won't discuss it today. Instead, we'll talk about the first two. Every programmer performs them before starting to work. You don’t just start coding without deciding what you are actually writing: a browser or a database. A clear understanding of the goal must be present. You must think through what exactly the program will do, rather than writing haphazardly in the hope that the code will somehow turn into a browser.
How exactly does this preliminary code planning happen? How much effort should we spend on it? It all depends on how complex the problem we are solving is. Let’s assume we want to write a fault-tolerant distributed system. In this case, we should think everything through carefully before sitting down to code. But what if we just need to increment an integer variable by 1? At first glance, this seems trivial, and no thought is required, but then we remember that overflow can occur. Therefore, even to determine whether the problem is simple or complex, we need to think initially.
If you think through possible solutions to a problem in advance, you can avoid mistakes. But for this, your thinking must be clear. To achieve this, you need to write down your thoughts. I really like the quote from Dick Hinton: “When you write, nature shows you how untidy your thinking is.” If you don’t write, you only think you are thinking. And you must write down your thoughts in the form of specifications.
Specifications serve multiple functions, especially in large projects. But I will only discuss one of them: they help us think clearly. Clear thinking is very important and quite difficult, so we need any support here. In what language should we write specifications? This is always the first question for programmers: in what language will we write? There is no single correct answer: the problems we solve are too diverse. For some, TLA+ is useful — it is a specification language I developed. For others, Chinese is more convenient. It all depends on the situation.
A more important question is: how can we achieve clearer thinking? The answer is: we must think like scientists. This way of thinking has proven effective over the last 500 years. In science, we build mathematical models of reality. Astronomy was perhaps the first science in the strictest sense of the word. In the mathematical model used in astronomy, celestial bodies are represented as points with mass, position, and momentum, although in reality they are extremely complex objects with mountains and oceans, tides and ebbs. This model, like any other, is created to solve specific tasks. It is well-suited for determining where to direct a telescope if you need to find a planet. But if you want to predict the weather on that planet, this model won't work.
Mathematics allows us to determine the properties of the model. And science shows how these properties relate to reality. Let's talk about our science, computer science. The reality we work with consists of computational systems of all kinds: processors, gaming consoles, computers executing programs, and so on. I will talk about executing a program on a computer, but, broadly speaking, all these conclusions apply to any computational system. In our science, we use many different models: Turing machines, partially ordered sets of events, and many others.
What is a program? It is any code that can be considered on its own. Suppose we need to write a browser. We have three tasks: design the program's presentation for the user, then write a high-level scheme of the program, and finally, write the code. As we write the code, we realize that we need to create a tool for formatting text. Again, we need to solve three tasks: determine what text this tool will return; choose an algorithm for formatting; write the code. This task has its own subtask: to correctly insert hyphens into words. We also solve this subtask in three steps— as we see, they repeat at many levels.
Let's take a closer look at the first step: what task the program is solving. Here, we often model the program as a function that receives some input and produces some output. In mathematics, a function is typically described as an ordered set of pairs. For example, the squaring function for natural numbers is described as the set {, , , , ...}. The domain of such a function is the set of the first elements of each pair, i.e., the natural numbers. To define a function, we need to specify its domain and formula.
However, the functions in mathematics are not the same as functions in programming languages. Mathematics is significantly simpler. Since I don't have time for complex examples, let's consider a simple one: a function in C or a static method in Java that returns the greatest common divisor of two integers. In the specification of this method, we will write: computes GCD(M,N) for arguments M and N, where GCD(M,N) — the function whose domain is the set of pairs of integers, and whose return value is the largest integer that divides M and N. How does this model correlate with reality? The model operates with integers, while in C or Java we have 32-bit int. This model allows us to determine if the algorithm is correct GCD, but it does not prevent overflow errors. A more complex model would be needed for that, which there is no time for.
Let's talk about the limitations of a function as a model. The operation of some programs (for example, operating systems) is not just about returning a specific value for specific arguments; they can run continuously. Moreover, the function as a model is poorly suited for the second step: planning the method of solving the task. Quick sort and bubble sort compute the same function, but they are completely different algorithms. Thus, to describe how the program achieves its goals, I use a different model, which we will call the standard behavioral model. In this model, the program is represented as a set of all permissible behaviors, each of which, in turn, consists of a sequence of states, and a state is an assignment of values to variables.
Let's take a look at what the second step of Euclid's algorithm will look like. We need to calculate GCD(M, N). We initialize M as x, and N as y, then repeatedly subtract the smaller of these variables from the larger until they are equal. For example, if M = 12, and N = 18, we can describe the following behavior:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
And if M = 0 and N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Here, it's worth making a small digression about productivity. It is often measured in the number of lines of code written in a day. But your work is significantly more valuable if you have eliminated a certain number of lines, as it results in fewer bugs. And eliminating code is easiest to do in the first step. It's quite possible that you don't need all those features you're trying to implement. The quickest way to simplify a program and save time is not to do things that are not worth doing. The second step is second in potential for time saving. If you measure productivity in terms of lines written, then thinking through how to accomplish a task will make you less productive, as you can solve the same problem with a smaller volume of code. I cannot provide exact statistics here, as I have no way to count the number of lines I didn't write because I spent time on specification, that is, on the first and second steps. And it's impossible to conduct an experiment here either because, in an experiment, we aren't allowed to complete the first step; the task is defined in advance.
In informal specifications, it is easy to overlook many difficulties. There’s nothing difficult about writing strict specifications for functions; I won’t discuss that. Instead, we will talk about writing strict specifications for standard behavioral models. There is a theorem that states that any set of behaviors can be described using a safety property (safety) and a liveness property (liveness)Safety means that nothing bad will happen, the program will not give an incorrect answer. Viability means that sooner or later something good will happen, i.e., the program will eventually provide the correct answer. Generally, safety is a more important indicator; errors often occur here. Therefore, to save time, I will not discuss viability, although it is certainly important as well.
We achieve safety by specifying, first, a multitude of possible initial states. And, secondly, the relationships with all possible subsequent states for each state. We will act like scientists and define the states mathematically. The set of initial states is described by a formula, for example, in the case of the Euclidean algorithm: (x = M) ∧ (y = N). For certain values M and N there 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 prime, while those of the current state are written without a prime. In the case of the Euclidean algorithm, we will deal with the disjunction of two formulas, one of which x is the maximum value, while the other is y:
In the first case, the new value of y equals the previous value of y, and the new value of x is obtained by subtracting the smaller variable from the larger one. In the second case, we do the opposite.
Let’s return to the Euclidean algorithm. Let’s assume again that M = 12, N = 18. This defines a unique initial state, (x = 12) ∧ (y = 18). We then substitute these values into the formula above and get:
Here the only possible solution is: x' = 18 - 12 ∧ y' = 12, and we get the behavior: [x = 12, y = 18]. Similarly, we can describe all states in our behavior: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In the final state [x = 6, y = 6] both parts of the expression will be false, hence there is no subsequent state. So, we have a complete specification of the second step — as we see, this is quite ordinary math, like what engineers and scientists do, rather than something strange, as in computer science.
These two formulas can be combined into a single temporal logic formula. It is elegant and not difficult to explain, but there is no time for that now. Temporal logic may only be necessary for the liveness property, as it is not needed for safety. Temporal logic as such is not preferred; it is not quite ordinary mathematics, but in the case of liveness, it is a necessary evil.
In Euclid's algorithm for each value x and y there are unique values x' and y', which make the relation to the next state true. In other words, Euclid's algorithm is deterministic. To model a nondeterministic algorithm, the current state needs to have several possible future states, and each value of the variable without a tick must have several values of the ticked variable for which the relation to the next state is true. This is not difficult to do, but I will not provide examples right now.
To create a working tool, formal mathematics is needed. How do we make a formal specification? For this, we will need a formal language, such as . The specification of Euclid's algorithm will look as follows in this language:
The symbol of equality with a triangle means that the value on the left side of the symbol is defined as equal to the value on the right side. Essentially, a specification is a definition; in our case, two definitions. To the TLA+ specification, we need to add declarations and some syntax, as shown on the slide above. In ASCII, it will look like this:
As we can see, nothing complicated. A specification in TLA+ can be checked, i.e., all possible behaviors can be explored in a small model. In our case, this model will consist of specific values M and N. This is a very efficient and straightforward verification method that is performed entirely automatically. Additionally, formal proofs of truth can be written and mechanically checked, but this takes a lot of time, which is why hardly anyone does it.
The main drawback of TLA+ is that it's mathematics, and programmers and computer scientists fear mathematics. At first glance, this may sound 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 formulas appeared on the screen, their eyes went glassy. So if TLA+ is intimidating, you can use , which is a kind of toy programming language. An expression in PlusCal can be any expression of TLA+, that is, fundamentally, any mathematical expression. Moreover, PlusCal has syntax for nondeterministic algorithms. Because you can write any TLA+ expression in PlusCal, it is significantly more expressive than any real programming language. Additionally, PlusCal compiles into an easily readable TLA+ specification. This doesn’t mean that a complex PlusCal specification will turn into a simple one in TLA+ — the correspondence between them is clear, and no additional complexity will arise. Finally, this specification can be verified using TLA+ tools. In short, PlusCal can help overcome the fear of mathematics; it's easy to understand even for programmers and computer scientists. In the past, I published algorithms in it for about 10 years.
Some may argue that TLA+ and PlusCal are mathematics and that mathematics only works on invented examples. In practice, however, a real language with types, procedures, objects, and so on is needed. This is not true. Here’s what Chris Newcomb, who worked at Amazon, says: “We used TLA+ in ten large projects, and in each case, its use made a significant contribution to development because we were able to catch dangerous bugs before they reached production, and because it gave us the understanding and confidence needed for aggressive performance optimizations that do not affect the correctness of the program.”It is often heard that using formal methods results in inefficient code — in practice, the opposite is true. Furthermore, there is a common belief that it is impossible to convince managers of the necessity of formal methods, even if programmers are convinced of their usefulness. And Newcomb writes: "Managers are now encouraging the writing of specifications in TLA+, and are specifically allocating time for it". So when managers see that TLA+ works, they gladly embrace it. Chris Newcomb mentioned this about six months ago (in October 2014), and now, as far as I know, TLA+ is used in 14 projects instead of 10. Another example relates to the design of the Xbox 360. Charles Tecker had an intern come in and write a specification for the memory system. Thanks to this specification, a bug was found that otherwise would have gone unnoticed and would have caused every Xbox 360 to crash after four hours of use. Engineers at IBM confirmed that their tests would not have detected this bug.
You can read more about TLA+ online, but now let's talk about informal specifications. We rarely write programs that compute the greatest common divisor and the like. Much more often, we write programs like the pretty-printer tool that I created for TLA+. After the simplest processing, the code in TLA+ would look like this:
But in the given example, the user likely wanted the conjunction and equality signs to be aligned. So the correct formatting would look more like this:
Let's consider another example:
Here, on the contrary, the alignment of equality, addition, and multiplication signs in the source was random, so the simplest processing is quite sufficient. In general, there is no exact mathematical definition of correct formatting because "correct" in this case means "the way the user wants it," which cannot be mathematically defined.
It might seem that if we don't have a definition of truth, then the specification is useless. But that's not true. Just because we do not know exactly what the program should do, it does not mean that we should not think through its operation—on the contrary, we should spend even more effort on this. The specification is especially important here. It is impossible to define the optimal program for pretty-printing, but that does not mean we should not attempt it at all; writing code as a stream of consciousness is not the way to go. In the end, I wrote a specification consisting of six rules with definitions in the form of comments in the Java file. Here's an example of one of the rules: a left-comment token is LeftComment aligned with its covering token. This rule is written in what you might call mathematical English: LeftComment aligned, left-comment and covering token — terms with definitions. This is how mathematicians describe mathematics: they write definitions of terms and based on that — rules. The advantage of such a specification is that it's significantly easier to understand and debug six rules than 850 lines of code. I must say, writing these rules was no easy task; a considerable amount of time was spent debugging them. Specifically for this purpose, I wrote code that indicated which exact rule is being used. Because I tested these six rules on several examples, I didn't have to debug 850 lines of code, and the bugs turned out to be quite easy to find. Java has excellent tools for this. If I had just written the code, it would have taken me significantly more time, and the formatting would have been of lower quality.
Why couldn’t formal specification be used? On one hand, the correctness of execution here is not too important. A structural printout will inevitably not satisfy someone, so I didn’t need to ensure correct operation in all extraordinary situations. More importantly, I did not have adequate tools. The tool for checking TLA+ models is useless here, so I would have to write examples manually.
The given specification has characteristics common to all specifications. It is at a higher level than code. It can be implemented in any language. Any tools or methods are useless for writing it. No programming course will help you write this specification. And there are no tools that could make this specification unnecessary unless you are writing a language specifically for producing structural printouts in TLA+. Finally, this specification says nothing about how we will write the code; it only states what this code does. We write specifications to help us think about the problem before we start thinking about the code.
But this specification also has features that distinguish it from other specifications. 95% of other specifications are significantly shorter and simpler:
Furthermore, this specification serves as a set of rules. Generally, this is a sign of a poor specification. Understanding the consequences of a set of rules can be quite difficult, which is why I had to spend a lot of time debugging them. Nonetheless, in this case, I couldn't find a better way.
It’s worth saying a few words about programs that run continuously. Typically, they operate in parallel, such as operating systems or distributed systems. Very few can grasp them mentally or on paper, and I am not among them, although I once had that capability. Therefore, tools are needed to verify our work — for instance, TLA+ or PlusCal.
Why write a specification when I already knew what the code was supposed to do? In reality, I only thought I knew. Additionally, with a specification in place, an outsider no longer needs to dive into the code to understand what it does. I have a rule: there should be no general rules. This rule, of course, has an exception — it is the only general rule I follow: the specification of what the code does should convey to people everything they need to know when using that code.
So, what exactly do programmers need to know about thinking? To begin with, the same thing as everyone else: if you're not writing, you only think you're thinking. Moreover, you need to think before coding, which means you need to write before coding. A specification is what we write before we start coding. Specifications are necessary for any code that may be used or modified by someone else. And that "someone else" could be the author of the code themselves a month after writing it. Specifications are needed for large programs and systems, for classes, for methods, and sometimes even for complex sections of an individual method. What exactly needs to be written about the code? You need to describe what it does, that is, what could be useful to anyone using this code. Sometimes, it may also be necessary to specify how exactly the code achieves its goal. If we covered that method in an algorithms course, we call it an algorithm. If it’s something more specific and new, we call it high-level design. There is no formal difference here: both are abstract models of a program.
How exactly should you write a specification for code? The main point: it should be a level above the code itself. It should describe states and behaviors. It should be as strict as the task requires. If you're writing a specification for how to implement a task, it can be written in pseudocode or using PlusCal. You need to learn to write specifications based on formal specifications. This will give you the necessary skills that will also help with informal ones. So how do you learn to write formal specifications? When we learned programming, we wrote programs and then debugged them. The same applies here: you need to write a specification, check it using a model checker, and correct any errors. TLA+ might not be the best language for formal specifications, and another language might suit your specific needs better. The advantage of TLA+ is that it teaches mathematical thinking exceptionally well.
How to link specifications and code? Through comments that connect mathematical concepts to their implementation. If you're working with graphs, you will have arrays of nodes and arrays of connections at the program level. Therefore, you need to describe how exactly the graph is implemented with these programming structures.
It's important to note that none of the above pertains to the actual process of writing code. When you write code, which is the third step, you also need to think and plan the program. If a subtask turns out to be complicated or unclear, you need to write a specification for it. However, I'm not discussing the code itself here. You can use any programming language, any methodology; this isn't about them. Moreover, nothing stated above eliminates the need to test and debug the code. Even if the abstract model is correctly written, there could be bugs in its implementation.
Writing specifications is an additional step in the coding process. Thanks to it, many errors can be caught with less effort — we know this from the experiences of programmers at Amazon. With specifications, the quality of programs increases. So why do we often do without them? Because writing is difficult. And writing is difficult because it requires thinking, and thinking is also hard. It's always easier to pretend you're thinking. There's an analogy here with running — the less you run, the slower you become. You need to train your muscles and practice writing. Practice is essential.
Specifications may be incorrect. You might have made a mistake somewhere, or the requirements could have changed, or it may have been necessary to make improvements. Any code that someone uses has to be adjusted, so sooner or later the specifications will no longer match the program. Ideally, in this case, a new specification should be written and the code completely rewritten. We all know that this is rarely done. In practice, we patch the code and possibly update the specification. If this is inevitably happening sooner or later, then why write specifications at all? First, for the person who will edit your code, every extra word in the specification will be precious, and that person can very well be you. I often scold myself for not having enough specification when I edit my code. I write more specifications than I do code. Therefore, whenever you edit the code, the specification always needs to be updated. Second, with each edit, the code gets worse; it becomes increasingly difficult to read and maintain. This is an increase in entropy. But if you don't start with a specification, then every line you write will be an edit, and the code will be bulky and hard to read from the very beginning.
As said , , no battle was won according to plan, and no battle was won without a plan.And he knew a thing or two about battles. There is an opinion that writing specifications is a waste of time. Sometimes this is indeed the case, and the task is so simple that there is nothing to think through. But always remember that when you are advised not to write specifications, it means you are being advised not to think. And this is something to consider every time. Thinking through a task does not guarantee that you won't make mistakes. As we know, no magic wand has been invented, and programming is a complex undertaking. But if you don't think through the task, you are guaranteed to make mistakes.
You can read more about TLA+ and PlusCal on a special site, which you can access from my homepage . That's all from me, thank you for your attention.
Just a reminder that this is a translation. When you write comments, please remember that the author will not read them. If you really want to communicate with the author, they will be at the Hydra 2019 conference, which will be held on July 11-12, 2019, in St. Petersburg. Tickets can be purchased .
Source: habr.com
