Turing Award Winner On Thinking Clearly, Paxos vs Raft, Working With Dijkstra | Leslie Lamport

33:03And I think realized it was because of that cute story that that problem was popular. And so I decided that, you know, our work needed a cute story, a nice story, and I invented Byzantine generals, the idea being that you have a group of, you know, for the one failure case, you have four generals who have to agree whether or not to attack. And if they all attack, they'll win the battle. But if only some of them attack, or even if three of them attack, they'll win the battle. But if only two attack, they would lose. But one of the generals might be a traitor. And so how could you solve this problem?

33:53And so it's phrased in terms of these generals having to communicate and decide whether to make the single decision, whether to attack or retreat. And, you know, I called it the Byzantine generals problem.

34:11Leslie Lamport:I saw in your notes about the problem that there was maybe a subset of the problem or a prior version that was called the Chinese generals problem or something like that. Oh, yeah. There's a different problem that Jim Gray described as an impossibility result, basically. It's called the Chinese general problem. I won't bother going into what it is. And so that gave me the idea of generals. I actually originally thought of the idea of Albanian generals, because at that time, Albania was a black hole as far as the rest of the world was concerned. It was a communist regime, it's a part of the Soviet bloc, but it was even more Soviet than the Soviet Republican and more restrictive.

35:07So when my boss said, well, you know, there are Albanians in the world, so you shouldn't have that, and so it should have a different name. And then I realized that Byzantine, there aren't any Byzantiums, Byzantines around. And that was the perfect name.

35:25Leslie Lamport:It's interesting to me in the story that, because this isn't the first time the problem was specified, but it's the first time that you named it, gave it a good catchy name essentially, and added some additional results. What was it that you saw in that problem that made it interesting or rather like how do you know that a problem is worth putting extra time into oh well this one it was because you know the it was obvious that people were going to be building that computers were going to fly or airplane fly airplanes and the reason in fact because was was that this was during the time of the oil crisis in the 70s and that they knew people knew that they could build more energy efficient planes by reducing the size of the control surfaces, but that made the plane aerodynamically unstable, and a pilot couldn't make all the adjustments needed to keep it flying, but a computer could.

36:30So it was clear the future was, you know, airplanes were going to be flown by computers, as they are, you know, today.

36:42and people didn't realize, they thought that, oh, if you want to be able to tolerate one fault, you just use three computers and they didn't realize that, you know, with arbitrary faults, you need four and so that was a really important result and that's why I believe that it needed to be well known.

37:03Leslie Lamport:Generally, when you look at the problems that you are solving with your work, how'd you decide because if you're working at a company you can decide based off of maybe the I guess the impact of the company like is it going to make more money or save costs or something like that but I wonder in your work across your career you know think about the bakery problem or some of your later work as well how do you know it's it's so open-ended how do you know which problems are the ones worthwhile? Throughout my career, I worked for private companies, you know, and not, you know, not in academia or for the government.

37:45And so some problems arose because of, you know, sometimes, you know, an engineer would have a problem and come to me. And so, you know, Disc Paxos, for example, was a case of that, that somebody actually wanted an algorithm to do what it did.

38:05Leslie Lamport:You mentioned earlier Paxos, and I know that's one of your most famous works. Curious about the story behind maybe that paper and the problem you're solving? Well, the problem I was trying is exactly the same problem as I was solving in the Byzantine General's work, basically building a fault-tolerant state machine. But by that time, the faults that interested industry were ones where failure meant that the computer just stopped, not that it did arbitrary things. So Paxos is an algorithm for building fault-tolerant systems for handling that class of faults. And the people I was working at was the Dexerc lab, which I joined in 1985.

39:06And they built a, what are the first operating systems that was a distributed operating system so that, basically everybody had basically these are the people who had come from Xerox Park and had invented personal computing but they also had the notion of distributed personal computing they invented the Ethernet you know for that so they basically all of the computers in the building were on a single Ethernet network and shared a common storage and they had an algorithm for maintaining consistency of that storage. And I didn't believe, well, they didn't have an algorithm. They had an operating system with code that did that.

40:05And I didn't believe that what they did was possible. Namely, I didn't think,

40:19well I forget exactly why I didn't think it was possible but at any rate I started trying to come up with an impossibility proof and then started solving proof well an algorithm to solve this would have to do this and in order to do this it would have to do that and at some point I stopped and said oh this isn't a proof this is an algorithm that does it

40:45Leslie Lamport:You said that they had code, but not an algorithm. Yeah. What do you mean by that? When most people sit down and start writing programs, they start by thinking in terms of code. And one of the things I learned fairly early in my career, I don't remember exactly when, that back in the days when I started writing concurrent algorithms, people talked about, people were calling them programs. And I was probably calling them programs too. I mean, I remember. Then at some point I realized that I wasn't talking about programs. I was talking about interested in algorithms. And an algorithm is something that's more abstract than a program.

41:35an algorithm can be a program is written in some particular code but an algorithm can be implemented in programs written in any kinds of code it's something that's at a higher level of abstraction and of course I like that because abstraction is something I was good at even without realizing that that's what I was doing and so So what I've spent a large part of my career, basically maybe about 2000 or so onward, was getting people who build concurrent systems to not just write code, but to have an algorithm. Now, a system does lots of things, but there should be some kernel of the program that's involved with synchronizing the different processes or the distributed system, the different computers.

42:45And that code is very hard to get that correct. So you don't want to think in terms of code because that encoding, you know, conflates, you know, a lot of issues that are irrelevant to the concurrency aspect. And so you should be thinking, you know, first get an algorithm that does that synchronization and then implement that algorithm.

43:12Leslie Lamport:I was looking at the Paxos paper and some of your notes about it. And I saw that there's an eight-year gap between when you came up with the algorithm and when the paper was actually published called Part-Time Parliament is the name of the paper. Why is there an eight-year gap? Oh, well, the referees originally said, well, this paper is okay, you know, not terribly important. But fortunately, Butler Lamson realized the importance of the algorithm. And together with the idea of, you know, I guess you can implement anything because it's implementing a state machine. And, you know, went about proselytizing, building your systems, you know, using Paxos, you know, and thinking in terms of state machines.

44:09And so, you know, I wasn't... So the idea was getting out, so I was in no hurry to publish. So, you know, I just let the paper sit. And eventually there was a new editor that came along and he said that, you know, I think the status of the paper was that it was just, you know, it had been accepted but it needed revision. And so he decided that, yeah, let's, you know, publish it. And it was eventually published with a few things to mention work that had been done in the interim. And what I got is Keith Marzullo to do that part for me. and so the story was that this manuscript, this was that, well, the story about Paxos was that, you know, this happened, you know, centuries ago and, you know, this manuscript and I used that to the effect that, you know, when something, you know, the tales of something were I considered obvious and not interesting, you know, the paper would say, it's not clear how the Paxos, what the Paxons did, you know, at this point, But at any rate, and so Keith, you know, kept up that idea that, you know, this was a, you know, a description of this ancient thing.

45:52And he wrote, you know, a little prefix or a preface or something to it and, you know, added maybe, I think, some references.

46:02Leslie Lamport:I saw in your writing, too, when you were talking about presenting the paper initially, you even dressed up in like an Indiana Jones-style archaeologist. Well, how did that go when you presented about this Paxos paper and algorithm? Well, I think the lecture may have gone well, but I think nobody understood the algorithm where nobody understood the significance of the algorithm. It sounds like no one understood it except for Butler Lamson. And what did he see that made him unique, I guess? Well, he had a good understanding of building systems. You know, he really deserved his touring award. He was one of the original people at Xerox Park who were building distributed personal computing.

46:49He and Chuck Thacker, I think, were probably the two senior people in that lab.

46:56Leslie Lamport:I saw later there was a paper which describes a new algorithm which seems to solve the same problem, the RAFT paper. I was wondering if you read that and what your thoughts were on that versus Paxos. The authors of that actually sent me a draft of the original paper, and I looked at it and said, I forget whether I said, send it back to me when you have an algorithm or send it back to me when you have a proof. I forget which one it was. And I got the idea, and they did write, you know, add a proof in the paper. and I never read later versions. And someone whose judgment I value had read it and said that it's basically the Paxos paper, but with some of the details left unfinished by the Paxos paper, by some of the details filled in.

48:01but they described it in a very different way. The basic idea of what Paxos works is it's two phases, and you're trying to implement a sequence of decisions. And it turns out you can do the first phase once. It involves a leader, and the leader has to get elected. But it turns out that you can do the first phase once and you don't have to do it again as long as you have the same leader. But it's only the second part that you have to do and then you have to elect the new leader if the new leader fails and do the first part. So think about it in those two phases. But the way people, the way engineers seem to like to think about it is, well, you do this, you know, you're talking about the first part, the second phase, you keep doing this until the leader fails, and then you go back, then you have to do this thing.

49:16So it's explaining it in the opposite order. and in fact when you started from fresh you don't have to do the first the first phase you can basically what started the first phase could be just built into the initial state but I think that those two phases is the way to understand it but you know the raft people also had this idea that raft is better because it's simpler. I must say that a lot of people say that Paxos is hard to understand, and I don't understand why. I mean, I've explained it to people in five minutes, and they understood it. At any rate, the RAF people said that one of the ideas were simpler, because, and they even have, you know, taught, you know, Paxos to one class, and RAF to another, and they took, and then, yes, the people, all the students said that, yes, it was more understandable.

50:20The interesting thing about it, though, is that there was a bug discovered in Raft and fixed, but I believe that the algorithm that they found more understandable was one with that bug. so uh made me realize that uh you know what most people you know what does understanding mean and for me understanding means you know you can write a proof of it but what understanding means for most people is a warm fuzzy feeling and you know the raft description gave them you know more of a warm fuzzy feeling because you know you know that that was seems to be the way Many programmers like to think about the algorithm, the second phase first until you get a failure.

51:19But the way I describe it is one that helps you get a better understanding of why it actually works.

51:26Leslie Lamport:So, yeah, we talked about a lot of your papers. I know one of your other contributions, whether you knew it or not at the time, was LaTeX. and building that and something that has impacted the entire academic community. What's the story behind wanting to build LaTeX? Oh, that was very simple. I was in the process of starting to write a book, and it was clear that tech was the basic typesetting system that one had to use. But, you know, I felt that I would need macros to make tech do what I wanted it to do. And so I decided, figured with a little extra effort, I could make the back rows usable by other people.

52:30The system I had been using before tech was called Scribe. And that really had the basic idea of Scribe was that you describe the logical structure of the document, and Scribe will do the formatting. Well, Scribe didn't do that great a job of formatting.

52:59But obviously, I like the idea, abstraction, that it's the ideas that matter, not the text, the writing that matters, not the typesetting. And so I actually, at some point, I met Peter Gordon, Addison Wesley. I'm not sure what you would call him, but he looks for books to publish. And he convinced me that I should write a book on it. And those days, it never occurred to me people would actually spend money for a book about software. but you know what the hell and what he did was he introduced me to a typographic designer at Addison Wesley who was responsible for really for the typographic design that's in the standard playtex styles you know basically I just did that in my quote spare time you know took me six or nine months or so.

54:10I suppose the statute of limitations has run out, but I was really, you know, spent some time working on that when I was allegedly, you know, billing the time to some project that had nothing to do with it.

54:25Leslie Lamport:On the topic of writing, you have a quote that I really enjoy. It's, if you're thinking without writing, you only think you're thinking. And I was curious to hear your thoughts on what you mean by that. Well, it was really meant for people building computer systems. You have an idea and you think it's going to work, or you have something that you think is something that somebody else will want to use. Well, write a description of it. There's an old maxim that I heard. that is, you know, write the instruction manual before you write the program. Great advice. I did not do that with LaTeX, but I definitely, when I was writing the book and I discovered that something was hard to describe, hard to explain, that needed to be changed.

55:26And I made, you know, a number of changes to it. as a result of that. But I didn't start at the beginning with the instruction manual.

55:36Leslie Lamport:Why is writing conducive to good thinking? Because it's very easy to fool yourself. I mean, that underlies my whole idea of writing proofs. One thing I learned is that you had to write a correctness proof of a concurrent algorithm. And when my algorithm was starting to get more complicated, the proof started, I started to write, you know, I was a math, a PhD in math, I knew how to write proofs. And I was starting writing the proofs the way I would normally do. And I realized it just didn't work because there were just so many details involved. And I just couldn't keep track of them and whether I had done it.

56:30And so, as a computer science, you know how to deal with concurrency. It's hierarchical structure. And so I devised this hierarchical structure where a proof is, you know, is a sequence of steps, each of which has a proof. And the proof is either a, well, a proof is either a paragraph or a sequence of steps, each with its proof. And that proof can be either a paragraph or a sequence of steps with its proof. So you break the whole problem up into these smaller pieces. So there's never any question of where is this coming from. You're stating that this step follows from this step, this step, this step, this step.

57:15And if it does not follow from that step, your proof is wrong. The theorem might be correct, but it means your proof is wrong. Well, you know, I discovered that worked great on writing my proofs of programs. But I decided to really, you know, I also write proofs of theorems. You know, think proofs that are things that are more like ordinary math. And I started trying that on them. And I discovered it worked beautifully. So when I started to try to convince mathematicians to write these proofs, I started in one small seminar. I won't describe what it was about, but I described this proof through maybe 20 mathematicians or something.

58:04Their reaction shocked me. They became angry. I really thought that they might physically attack me. So I believe that what's going on is that when people, I mean, I believe that's totally irrational. And when people act irrationally, it tends to be out of fear. And what I believe people are afraid of is, the mathematicians are afraid of, is that they're going to have to write their proofs to convince a computer program. And in fact, you know, and I give it one of those talks I gave, you know, I say very clearly, this doesn't have to be, You don't have to be any more formal than you do. You can write the exact same thing, proof, but it's just a matter of organizing things.

58:58And it's very simple, you know, hierarchical structure. And then when you're using a fact, mention that you're using that. Nothing about formalism or anything. You know, after I gave that talk, someone got up and said, I don't want to have to write my proofs for a computer program. And in fact, it's more work doing that because the reason it's more work is that it reveals what you haven't said. And that there's steps in there that you may think they're obvious, but you haven't written them down. And if you believe something is correct, but don't really, if you think you know something, but don't write it down, you only think you know it.

59:50And that's where errors come in. That's where that one third of the paper's errors come in. Because it really makes you honest.

1:00:01Leslie Lamport:When I look across your career, I think you had a lot of contributions people might expect might come from academia, these papers and things, but you did all of your work in industry. Why did you not see yourself as an academic and more of working for industry? Well, I started out programming, and I eventually got jobs where it took me into what we now call computer science. At the time, I never even realized that there could be a science of computing. It wasn't until, you know, maybe until mid to late 70s that I realized, yes, there was a computer science, and I was a computer scientist. but it never seemed to me that computer science was an academic subject.

1:00:57At some point I had to make a choice between doing computer science without calling it computer science or teaching math at a university. I chose for fairly random reasons to do computer science. so you know the first I don't know well till maybe the mid 80s or something it just didn't seem to me that you know computer science was something that people needed to go to a university to learn and I suppose afterwards that I was sort of I guess I just didn't think it would be fun teaching computer science.

1:01:48Leslie Lamport:I saw in your writing, you had a footnote that said somewhere that you felt like a failure at some point because you wanted to develop this grand theory of concurrency and you never discovered it. Do you still feel that way or what are your thoughts on that footnote? Lots of people, a large percentage of the people who were doing things like I was doing, which is not a large number of people, there's this notion that they're looking for the Turing machine of concurrency. The Turing machine was this abstraction which really captured what computing was.

1:02:32And they were looking for something that would be the Turing machine of concurrent computing.

1:02:47And, you know, nobody succeeded. I mean, there are some people who think they've succeeded. The patronets are something that I guess I don't have time to explain, but there was a big in the 70s, and I was actually surprised to think that there's still a large community of people doing patronets. but what I now realize is that patronets and most of the things that people were doing was really language-based. And I was never interested in languages. I'm interested in what the language is expressing. And, you know, I realized in some sense, you know, maybe I've realized what the Turing machine of computing is.

1:03:34It's state machines. state machines are a little bit different the way I now describe them they don't have commands, they just have a state and a next state relation even simpler than talking about commands and values and to me that's the Turing machine of concurrency but it it doesn't have the function that Turing machines offer, because what Turing machines do is describe what's possible. And state machines can describe anything, including things that are not possible. And in fact, there's a good reason for that. for example when I describe an algorithm I will talk about the values of a variable can be any integer now you can't implement the program where you have any integer but that makes but talking about computer integers would complicate things unnecessarily People have this funny idea that because something is infinite, it's more complicated.

1:05:08They got it backwards. Infinity was introduced to simplify things. The first thing you learn is arithmetic. You're learning arithmetic with an infinite number of integers because if you were restricted to a finite set of integers, arithmetic becomes much more complicated. So the abstractions of mathematics, which people find, because they don't have the proper training in mathematics, find difficult, are really what's simplifying things. And that's what you use, this mathematics. The state machine is described by me using mathematics. That's the right, you know, the most powerful way of doing it.

1:05:59But computer people and computer scientists and programmers are really hung up on languages. And so they are looking for, you know, they invent all sorts of languages. and they're all describable. And in fact, if you want to give them semantics, you would do it in terms of a state machine. And they just think that this, you know, this language improves your thinking. It doesn't. I mean, there are reasons why you use computer languages and you don't write your program's code in math. and they involve basically efficiency. But for understanding, you can't build math. You can't beat math. And, you know, attempts to do it by something that looks like a programming language is just the wrong way to deal when you're trying to deal with concurrency.

1:07:05Leslie Lamport:When I look at everything that you've written and all the stories, there's these little anecdotes. There's things where you say things like you never considered yourself smart, but you noticed that other kids had an awful time understanding things. Or, yeah, there's a problem that you solved where someone else had difficulties, but you don't view your contribution as a brilliant one or anything like that. And that doesn't connect with me because you've also won a Turing Award and done all these amazing things. So how could that be that you, you know, just merely discover things and are not smart, yet you've achieved so much?

1:07:48Well, this general thing that psychologists talk about is that when someone is good at something, they don't realize how good they are at it because it's simple to them. there's the opposite one that uh people who are bad at something think they're better than they are because they're bad at it or put a little bit more concisely stupid people think they're smart because they're too stupid to realize they're not my the gift that i have is not in some sense raw intelligence. It's abstraction. And it's only recently, you know, last 10 or so years that I realized how much better I am at that than other people, most other people.

1:08:49Leslie Lamport:At this point, you've experienced so much. And when you look back on your career, if you could go back to yourself when you just graduated college and give yourself some advice knowing what you know now, what would you say? One thing I've learned fairly early in my life is that I shouldn't waste time trying to answer questions that I don't have to answer. I don't think about what I should have done because that's a question that I don't have to answer. Thank you for listening to the podcast. It's a passion project of mine that I really enjoyed building. Another passion project that I've been working on kind of in secret is building an ergonomic keyboard that I wish existed.

1:09:37Leslie Lamport:And I finally have a prototype. So I'd love to show you what we've built. It's ultra low profile and ergonomic, and I couldn't find anything like it on the market. So that's why we built it. I'll put a link to the keyboard in the description. you can take a look and learn more about the project there. We could definitely use your support. Also, if you have any feedback for me about the show, I'd love to hear it. Comments on YouTube have led to guests coming on like Ilya Gregorik and David Fowler. I wasn't aware of them until someone dropped a comment. Also, feedback in the comments helped me learn to reduce the number of cliffhangers in the intros.

1:10:11Leslie Lamport:So your comments definitely make a difference. Please keep letting me know what you'd like to see more of in the show and I'll see you in the next episode.