Author | Li Mei
Editor｜Chen Caixian
Leslie Lamport may not be a household name, but to computer scientists he is the contributor behind some familiar “names”. For example , the Paxos algorithm, the typesetting program LaTeX, the specification language TLA+, the “bakery algorithm” and the “Byzantine generals problem” , etc.
Leslie Lamport revolutionized how modern computers talk to each other. In 2013, he was awarded the Turing Award for his work on distributed systems.
In a distributed system, multiple components on different networks coordinate to achieve a common goal. Internet search, cloud computing, and artificial intelligence all require the coordination of numerous powerful computing machines working together. Of course, this coordination will also make us encounter more problems.
Lamport once said, “A distributed system is a system in which the failure of a computer you didn’t even know existed would render your own computer unusable.”
One of the biggest sources of problems is “concurrent systems”, where multiple computing operations occur in overlapping time slices, which leads to a kind of ambiguity: which computer has the correct clock? In a seminal paper in 1978, Lamport introduced the concept of “causality”, using the perspective of special relativity to solve this problem. Two observers may disagree on the order of events, but if one event causes the other to happen, then the ambiguity is removed. Sending or receiving messages can establish a causal relationship between multiple processes. “Logical clocks” (now also known as Lamport clocks), provide a standard way to reason about concurrent systems.
Armed with this tool, computer scientists began to wonder how they could systematically make these connected computers larger without adding bugs. Lampor came up with an elegant solution: Paxos, a “consensus algorithm” that allows multiple computers to perform complex tasks. Modern computing could not exist without Paxos and its family of algorithms. The Paxos algorithm is now an industry standard.
Another contribution of Lamport was his creation of the document preparation system LaTeX in the early 1980s , which provided sophisticated methods for typesetting complex formulas and formatting scientific documents. Not only in mathematics and computer science, but in most scientific fields, LaTeX has become the standard for essay formatting.
In addition, Lamport’s specification language, TLA+, enables engineers to describe program goals in a precise, mathematical way. Since the 1990s, Lamport’s work has focused on “formal verification,” the use of mathematical proofs to verify the correctness of software and hardware systems. His outstanding contribution was the creation of a “specification language” called TLA+ (Temporal Logic of Actions). A software specification is like a blueprint or recipe for a program that describes how the software should operate at a high level. This is not always necessary because writing a simple program is like boiling an egg. But for a more complex, riskier task, requiring greater precision, writing such a program is the equivalent of preparing a nine-course feast. You need to prepare each component of each dish, combine them in a precise way, and serve them to each guest in the correct order. This requires precise recipes and instructions, written in clear and concise language, which can lead to misunderstandings when written in English prose. TLA+ uses precise mathematical language to prevent errors and avoid design flaws.
Taking your recipe or specification as input, a program called a model checker checks that the recipe is reasonable and works as expected, resulting in a dish that the chef wants. Before Lamport wrote the proper specs for programmers, he lamented that programmers often scrambled together a system, since chefs couldn’t prepare food for dinner parties without knowing whether their recipes were correct.
These achievements are not accidental. The 81-year-old computer scientist has unusual insights into how people use and think about software.
Recently, Quanta Magazine did an exclusive interview with Lamport to discuss his work on distributed systems. In the interview, Lamport talks about how the TLA+ language he created helps programmers build better systems, also talks about current problems in computer science education, and emphasizes the importance of mathematical thinking in computer science.
AI Technology Review has compiled this interview without changing the original intention for the readers.
Caption: Lamport visits the Computer History Museum in Mountain View, California
Quanta: Let’s start with Paxos because it’s a very influential algorithm. Can you talk about what drove you to start doing this work?
Lamport : At the time people used some code to build a system, and I had a hunch that what their code was trying to achieve was impossible. So I decided to try to prove it and come up with an algorithm that people should use in their systems.
Quanta: What was wrong with their original algorithm?
Lamport : They don’t have an algorithm, they just have a bunch of code. Few programmers think about problems in terms of algorithms. When trying to write concurrent systems, if you just write code and no algorithms, your program is bound to be full of bugs.
Quanta: The paper that introduced Paxos (“The Part-Time Parliament”) was not widely read at first . Why is this happening?
Paper link: https://ift.tt/aPlqjh3
Lamport : Probably because I like to explain things with stories, and I use Greek letters for characters. For example, in the paper, there is a cheese inspector named ΓωИΔα. As a mathematician, there are Greek letters all over the place, I just didn’t realize that those who weren’t mathematicians would be intimidated by them. This resulted in this paper that should have been seen not being seen.
So Paxos didn’t work very well in the beginning, but it did achieve its goals in the long run, because people call this series of consensus algorithms Paxos, not “viewstamped replication” (this is a computer scientist, Another name for a consensus algorithm by Turing Award winner Barbara Liskov).
Quanta: After so many years in distributed systems, what led you to create TLA+?
Lamport : In the 1970s, when people reasoned about programs, they were trying to prove properties of the program itself, which were expressed in programming languages. Later people realized that they really should have stated what the program was trying to accomplish in the first place—that is, the behavior of the program.
In the early 1980s, I realized that a practical way to write these higher-level specifications for concurrent systems was to write them as abstract algorithms. With TLA+, I was able to express them mathematically in a sufficiently rigorous way. It turned out that TLA+ really did a great job. It’s important not to try to write algorithms in programming languages: if you really want to get things right, you need to write your algorithms in mathematical terms.
Quanta: You said, “If you only think and don’t write, you only think what you think.” Is that what model checking is for?
Lamport : Model checking is a method of comprehensively examining all implementations of a small model of a system. It only shows the correctness of the model, not the correctness of the algorithm. When model checking goes to verify correctness, coding just generates code, it doesn’t test anything. Before model checking, the only way to ensure that an algorithm works is to write a proof.
In practice, model checking checks all executions of a small instance of the algorithm. If you’re lucky, you can check enough instances to give you enough confidence in the algorithm. But for the use of systems and algorithms of any scale, proofs can verify their correctness.
Quanta: It sounds like model checking is related to another method of program verification: interactive theorem proving using tools like Coq. How are they different?
Lamport : The purpose of Coq is to solve real mathematical problems, and it captures the reasoning that mathematicians do. For example, Georges Gonthier used it to prove the four-color theorem. After the proof of a mathematical proposition is verified by a machine, it is almost certain that the proposition is true.
TLA+ is not designed for mathematicians, but for engineers who want to prove the properties of their systems. In the 1990s, after spending about 15 years writing proofs of concurrent algorithms, I learned what needed to be done in order to prove the correctness of concurrent algorithms. TLA is a logic that allows the proof process to have a complete formality, and TLA+ is also a complete language based on TL logic.
Quanta: Specification languages like TLA+ are not widely used in industry, are they? Why do you think this is?
Lamport : I’m doing my best. But basically, programmers and many (if not most) computer scientists are intimidated by math. So its “marketing” is very difficult.
Plus, every project had to be rushed to completion. There’s an old saying, “There’s never enough time to do something perfect, but there’s always time to start over.” Because TLA+ involves upfront work, and new steps are added during the development process, this also leads to So it’s not widely used.
Quanta: Is the upfront work always worth it?
Lamport : It’s true that most code written by programmers around the world doesn’t need very precise statements about what it’s supposed to do. But some things are important and need to be kept right.
For example, when people make chips, they want the chip to work. When people build cloud infrastructure, they don’t want bugs that lose people’s data. For those applications that require precision, you need to be very strict. And you need something like TLA+, especially when it comes to the concurrency that usually exists in these systems.
Quanta: Do programmers tend to spend more time writing code than thinking about code?
Lamport : Yes, the importance of thinking and writing before writing code needs to be taught in an undergraduate computer science course, but it’s not. The reason is that there is no communication between those who teach programming and those who teach program verification.
As far as I can see, there are problems on both sides of this divide. People who teach programming don’t understand validation they need to know, and people who teach validation don’t understand how it should be applied and used in practice.
TLA+ won’t gain a lot of users until this gap is bridged. I hope I can at least make it clear to people who teach concurrent programming that they need TLA+. In that case, TLA+ may still hope to be used by more people.
Quanta: I sense that you are not very satisfied with your computer science education in recent years. Is it because you don’t pay enough attention to mathematics?
Lamport : Yes, in terms of mathematical thinking .
Quanta: So how would you structure your undergraduate program?
Lamport : I’m not an educator, so I don’t know how to teach them. But I know what people should learn. They shouldn’t be afraid of math. They may have learned a simple math but don’t know how to use it. They don’t know what’s good about it. They learn enough to pass the exam and then forget about it.
Quanta: Mathematicians often say they see beauty in mathematics. You started in the field of algorithms, so do you see the beauty of algorithms?
Lamport : I don’t think about it from an aesthetic point of view. I probably feel the same way as everyone else, but I just put it in different words. Regarding algorithms, I don’t think about beauty, but simplicity is what I value very much.
Reference link:
https://ift.tt/AIvtrdD
Leifeng Network
This article is reprinted from: https://www.leiphone.com/category/academic/Ta4Mj8maFPhsy0Dk.html
This site is for inclusion only, and the copyright belongs to the original author.