SE Radio 203: Leslie Lamport on Distributed Systems

Leslie Lamport spoke with SE Radio host Jeff Meyerson. Lamport won a Turing Award in 2013 for his work in distributed and concurrent systems. He also designed the document preparation tool LaTex. Leslie is employed by Microsoft Research, and has recently been working with TLA+, a language that is useful for specifying concurrent systems from a high level. The interview begins with a definition: a distributed system is a multiprocessor system in which the time required for interprocess communication is large compared to the time for events within a single processor–in other words, it takes longer for interprocess communication than it does for a process to look at its own memory. Alternatively, a distributed system is one in which processors communicate by sending messages. Leslie goes on to talk about how he became interested in distributed systems, and describes the story behind his paper about the Paxos algorithm. The goal of Paxos is to maintain consensus in an environment with unexpected faults (otherwise known as Byzantine faults). After the discussion of Paxos, Jeff asks Leslie about his recent talk “Thinking for Programmers,” which emphasizes the benefit of having a specification prior to writing actual code. “Specification” can mean a variety of things, but predicates and next-state relationships provide a mathematical rigor that is well-suited to distributed and concurrent systems. The conversation concludes with Jeff asking Leslie about how a programmer can build the mental resolve to work through a difficult problem.

Show Notes

Related Links

• Leslie Lamport’s home page
• 2013 Turing Award: http://amturing.acm.org/award_winners/lamport_1205376.cfm
• Time, Clocks, and the Order of Events in a Distributed System: http://www.stanford.edu/class/cs240/readings/lamport.pdf
• The Part-Time Parliament: http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-paxos.pdf
• Paxos: http://en.wikipedia.org/wiki/Paxos_algorithm
• Thinking for Programmers: http://channel9.msdn.com/Events/Build/2014/3-642
• TLA+, a specification language: http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html

Transcript

Transcript brought to you by IEEE Software

Jeff Meyerson 00:00:36 It’ss software engineering radio, the podcast for professional developers. Our guest today is Leslie Lamport. His accomplishments include a recent touring award for his work in distributed systems, as well as the document writing and formatting tool attack. Recently, Leslie has been focusing on TLA, which stands for temporal logic of actions. TLA plus is a specification language that is well suited for writing high level specifications of concurrent and distributed systems. Leslie Lamport thanks for coming on software engineering radio. My pleasure. So congrats on your recent touring award it’s for your work in the area of distributed and concurrent systems. How do you define the distributed system?

Leslie Lamport 00:01:18 Well, it’s not something I’ve thought about recently. The definition I used to have is it’s a multi-process system in which the time required for interprocess communication is large compared to the time taken for the event. The time between events in a single processor. In other words, where it takes a processor a lot longer to exchange messages with another processor than it does for it to access its own memory. But as I said, that was a definition that I made up about 30 or 40 years ago nowadays distributed systems seem to have evolved to mean, uh, systems in which processes communicate by sending messages.

Jeff Meyerson 00:02:13 Does that, does that change sort of your formalized definition of it, or do you think of that as more of like a newer applied definition?

Leslie Lamport 00:02:19 Uh, the formalism doesn’t really depend on the definition of distributed, uh, though that depends what you mean by formalism. Do you mean the, uh, what I’m talking about by formalism here is how you go about specifying and reasoning about a distributed system, which is no different from how you go about reasoning or specifying any other concurrent system.

Jeff Meyerson 00:02:54 Sure. Yeah, that makes sense. And when did you start thinking about distributed systems? And I know you said it was a while ago, but, um, so sort of what, what led you to, to thinking about them?

Leslie Lamport 00:03:06 I’m not sure when I started thinking about them. I think it was when I received a technical report by a Johnson and Thomas, the one that’s cited in my time clocks paper. I don’t remember offhand the title of that technical report, but I think it had something to do about a distributed databases. And anyway, I got that tactic report and that’s the first paper or thought I ever had about distributed systems as near as I can remember.

Jeff Meyerson 00:03:49 Do you remember it like peaking your interest in, in a certain way that was different than other subjects that you had studied prior?

Leslie Lamport 00:03:58 Not different, but I would say, uh, I guess it just, well the paper itself, uh, which led directly to the time clocks paper occurred because I observed that there was something not quite right in the way they had done things, uh, in particular that the algorithm they used had the effect of allowing a violation of causality. That is where two events that will event a causally influence event B yet in their algorithm event, B could be processed before event. A and the whole idea of the problem of that notion of causality came about because of my familiarity with special relativity. And I could, it was totally obvious to me looking at what was going on, that it was completely analogous to the situation in special relativity, where instead of as a special relativity causality had to do with whether or not one event could causally affect another dependent on whether or not information from one could physically reach the other because of the finite speed of transmission of light or put I’d put it a little bit more coherently in special relativity one event proceeded another, if it was possible to transmit information from the first event to the second event using beams of light.

Leslie Lamport 00:05:51 And it was clear to me that the corresponding concept that a distributed system is one event proceeded another event, if it was possible for information to flow from a vent a to event B by messages sent, uh, through the system.

Jeff Meyerson 00:06:16 Okay. Yeah. So, so that did that lead to, um, I guess the, your development of, of vector clocks and then, uh, from then on just your, your further developments in distributed systems.

Leslie Lamport 00:06:30 Well, it led to what I called logical clocks and some people now call landlord clocks, which are somewhat different from vector clocks, which is, was in development. Uh, I don’t remember by whom, but that happened not long after my, uh, time clocks paper. It had the effect on that paper had, uh, w was twofold first. It got me thinking about the notion of causality, uh, in distributed systems, which is what the paper was at time clocks paper was noted for. It also led me to realize that the algorithm that I came up with, which was, um, a modification of the algorithm by Johnson and Thomas applied, not just to the problem they was looking at, which was, as I recall, uh, distributed databases, but applied to any system. I realized that, and here, I’m not sure exactly what led to that realization, but the realization that any system can be described as a state machine and using the algorithm, that is my adaptation of the Johnson, Thomas algorithm, one could implement an arbitrary state machine in a distributed system.

Jeff Meyerson 00:08:00 Right. Okay. So when I took a distributed systems in college, I felt like the course material was divided into two sections. The first section was sort of material that we learned before we studied Paxos, and I felt like it sort of worked up to Paxos and then the rest of the material was, was related to Paxos and access itself. And my professor stated over and over again, the, the importance of the Paxos algorithm. Um, could you talk a bit about, about your Paxos algorithm and what it solves?

Leslie Lamport 00:08:35 Well, it was actually the second major step past the time clock paper, namely the time clocks paper implemented a state machine in a distributed system, assuming no failures. So

Leslie Lamport 00:08:56 Now the question was, how do you do it with failures? And that was one of the next things I did after the time clocks paper. Now in those days, computer networks didn’t really exist or they, they probably existed in the sense that their engineers had hooked computers together, but, um, they certainly weren’t very common and the,

Leslie Lamport 00:09:33 It wasn’t clear what direction practical networks would go. And so I considered the problem more or less than the abstract. And I had an intuitive sense that in order to deal with failures, when needed to use real time, the reasoning that led me to that was this very naive. It was the idea that the only way that you can tell that a process had failed, rather than that, it was just going very slowly, is that it didn’t do something in time. And that without a notion of time there, you really couldn’t talk about the notion of failure. And so the first algorithm that I came up with was one that was based on time. That is, it assumed a synchronous communication network, meaning that when the network, when in the absence of failure, uh, a message would be delivered within a fixed bounded length of time.

Leslie Lamport 00:10:53 And so if a message hadn’t arrived when it was supposed to, you could deduce that a failure had occurred. And using that, I came up with a, an algorithm that extended the time clocks idea to, uh, deal with failures. And again, since the notion of even what constituted the failure was not well developed, or there were, there was no standard idea of what kind of failure one should handle. I considered arbitrary failures, namely failures, in which processes not only could just stop working, but could actually compute the wrong result. These are also known as Byzantine. These, these are the faults that are now known as Byzantine faults. So, uh, I came up with an algorithm that handled Byzantine faults. Uh, that was shortly before I went to Sri and what I arrived at when I arrived at Sri, I learned that the people there were in fact, working on, uh, Byzantine failures and working on the exact sort of network that I had posited, namely there, Sri had a contract to design a very reliable, uh, computer system for flying airplanes. It was, uh, a NASA contract

Jeff Meyerson 00:12:31 And yeah.

Leslie Lamport 00:12:33 Being reliable meant that had to handle failures, which meant you had to have a network of, uh, separate computers, uh, since any individual computer could fail. And they realized that something that, that hadn’t been realized before, namely that the presence of Byzantine failures could really complicate matters and particular the obvious way of handling failures by majority voting, uh, namely that you have say three processors, and one of them makes a mistake. You can use voting on their outputs. And as long as two of them were correct, then you get the right result. And what they discovered was that didn’t work. And the failure of Byzantine in the presence of Byzantine failures, because if a process didn’t just compute the wrong answer, but it gave different answers. What were reported different answers to different processes, then that could really screw things up. And they proved that to handle one failed computer.

Leslie Lamport 00:13:55 You needed not three computers before computers. Well, it turned out that I had my algorithm actually handled one failure with three computers, but that’s because I was making an assumption or using something that the, they weren’t namely my algorithm depended on digital signatures, something which at that time, very few people had even heard about. But when I got there, basically what I had done was combined with what they had done and, um, appeared as a paper. Um, is this the part time parliament that you’re talking about? Know this was the reaching agreement and the presence of faults paper was the authors were, uh, Rob Shaw stack Marshall peas, and me, and that was the work that initiated Byzantine General’s. Um, I realized that this was an important problem and that the results in that paper were important. And in order to, uh, get it more widely appreciated, I invented the idea of describing the problem in terms of Byzantine genitals. And, uh, so we wrote another paper, uh, it had some new results, uh, the major result being a simpler way of look of presenting the algorithm without digital signatures in the original paper, but it introduced the terminology of Byzantine generals and Byzantine agreement. And I think that had a large, uh, that had a lot to do with the paper getting to be so well known and Byzantine agreement becoming such a popular problem.

Jeff Meyerson 00:15:53 Yeah. I wanted to talk a bit about the, um, the notion of, of, I guess, using allegory or metaphor, um, in order to, to describe these, um, these complex problems. So for example, your, your paper on, um, on Paxos w was the part time parliament, or, well, one of your papers on Paxos, the part-time parliament, um, and it’s, it’s this allegory about a Greek Island and the legislative process that the people of the Island use. Uh, and I guess I want to read like a small section from it, just so the listeners kind of get an idea of what this, what the paper, uh, lays things out in terms of, um, so one section from it is, um, as Paxos prospered, legislators become became very busy. Parliament could no longer handle all details of government. So a bureaucracy was established instead of passing a decreed to declare whether each lot of cheese was fit for sale.

Jeff Meyerson 00:16:54 Parliament passed a decree, appointing a chief inspector to make those decisions. So I just find it very interesting that, um, you know, this is like a sophisticated, like super important paper and you chose to describe it in these kind of story-like terms. Um, and I guess I’m curious how you chose to approach a problem in this manner. And if you thought it helped you, uh, explain the problem or, um, if you thought it would just help with, um, communicating the problem to other people, like I’m just trying to get some insight into your process for that.

Leslie Lamport 00:17:31 Okay. This happened well, uh, it all is due to, uh, square Dykstra. Uh, he has one problem that he introduced just called the dining philosophers problem. And it’s a problem that, to me, never seemed particularly interesting. I mean, Dykstra was a brilliant computer scientist and he did some marvelous things. And I think that the dining philosophers problem were among the least interesting things he did, but it became very popular and still known and talked about today because it had a cute story. In that case, the story was one of a group of philosophers sitting around a table and they were eating some complicated kind of spaghetti that required two forks. And there was one, four and eight. Each fork was shared between two philosophers and, uh, you know, pretty silly, but catchy and that caught people’s attention. So I think that’s behind my reason for introducing Byzantine generals.

Leslie Lamport 00:18:44 And I realized that a cute story could gain people’s attention and that worked great with Byzantine General’s. So when I devised the Paxos algorithm, I decided to do it again and came up with, uh, the Greek Island. Uh, basically that was a disaster. I, uh, I think it prevented, it delayed the appreciation of the algorithm by close to a decade, uh, about the one thing that it did achieve is gave the algorithm a nice short name Paxos, uh, so that probably helped. But other than that, it was a disaster I did make use of the analogy of the story to present technical ideas. For example, the, uh, in cheese inspector was my way of describing what is now known as leases, the idea of giving a resource to a processor, but giving it for a fixed amount of time so that in case the processor crashed or failed, you could then later, you know, give that resource to some other processor. So that’s a somewhat important idea in how you use Paxos to build a real system. And I presented that idea in terms of the, uh, what was it, the cheese SAR or, or, or something, uh, at any rate,

Jeff Meyerson 00:20:30 Did you think of any of these ideas as you were explaining things in these terms, or did you already have these ideas and you just turned them into the fictionalized?

Leslie Lamport 00:20:40 No, no. The, the ideas had nothing to do with this story. The story was just a way of presenting the ideas. Sure. I guess I’m

Jeff Meyerson 00:20:48 Just saying, like, once you were sort of in the mode of this storytelling, did you think of any, you know, fictional roles and, and you were like, Oh, you know, maybe, maybe I should actually invent a practical reason for why this character would exist in this.

Leslie Lamport 00:21:04 No, no, no. It was completely the other way around. Uh, and it was a disaster because I don’t think any readers, uh, well, very few readers understood that this jeez inspector was in fact, the description of, of leases and how they would be used in a, in a real system. Um, another trick I used taking advantage of the story that this was an ancient civilization discovered through archeological excavation when there were implementation details that I thought were pretty straightforward and not worth taking the time to, uh, discuss, I would say something like the, uh, archeological records did not indicate exactly how the, how the parliament did this. I don’t know if anybody, uh, you know, appreciated or understood what I was doing in that sense. Um, as far as I know, the one person who actually understood the paper, when he first read it was Butler Lampson, and it was, and he recognized its significance and it was basically due to his writing and lecturing about it, telling people that they should use Paxos that Paxos eventually got to be well known.

Jeff Meyerson 00:22:33 So when I was preparing for this interview, I watched a recent talk that you gave called thinking for programmers. And you emphasize the need to think before starting to write a program. And you said that in order to think, you have to write, if you want to think effectively, and you give the example of an architect, blueprinting, a house to draw an analogy with how a programmer must similarly write a spec in order to elucidate the solution that he’s trying to reach. So was the part time parliament, was that a spec for Paxos or was that, is that just like a, um, sort of a more, um, uh, elaborate, um, description of it that was maybe the opposite?

Leslie Lamport 00:23:20 Well, the paper told the story to explain what was going on, what the algorithm was accomplishing and a little bit about it to give a little idea of how it works, but that paper also included a very rigorous specification of the algorithm, which is purely mathematical and a correctness proof. That is a proof that it satisfied certain properties. So the story was there just to, in a misguided attempt to help people and understand the algorithm intuitively, but the actual algorithm, the actual specification, the algorithm was it, which was in the paper was quite rigorous and there was no story behind it. It was, uh, basically just mathematics.

Jeff Meyerson 00:24:15 Great. And could you talk a bit more about what you were trying to convey in your talk about thinking for programmers?

Leslie Lamport 00:24:23 I’ve come to the conclusion that a lot of the problems that exist in software and a lot of the problems that one encounters in writing and building a system, writing a program, those are problems that are caused by not thinking about what you were doing before starting to code. And I have a sense that if you’re building a complicated system, the battle is won or lost before a single piece of code is written. That is the success really depends on the conception of the problem, the design of the, of the system, not in the details of how it’s coded, uh, best way to, well, to give an example of that is suppose you want to write a sorting program. Well, if the only sorting algorithm, you know, is bubble sor uh, by the way, will listeners understand what bubble sword is or should I give it a simpler example?

Leslie Lamport 00:25:44 Okay. So, um, bubble sword is not a very efficient way of sorting. And if the only idea you have of how to sort is bubble sword, then it doesn’t matter how good a coder you are, no matter how wonderful, beautiful your code, how perfect it is, how wonderful your programming language. You’re not going to produce a very good sorting program because it’s been a sort slowly. So the way to write a good sorting program is to use a better algorithm, something like quick sword or heaps article or something like that. And so the idea of whether you’re going to write a good sorting program or not is decided upon not by how good your coding is, but by the basic algorithm you’re using and that algorithm is chosen, or it should be chosen before you start coding. You don’t want to try to design a new sorting algorithm, um, in C because that’s not the right level to be thinking of sorting algorithms.

Leslie Lamport 00:26:52 Well, there are many dimensions in which, uh, fundamental algorithms are fundamental. Design can differ. One of them is computational complexity, which is a fairly well now a fairly obvious one. And so if somebody is, has a well-defined algorithm that, Oh, I’m sorry, I’m well-defined problem. That’s, that’s been well studied such as sorting or maybe computing various things on graphs. Well, he knows to go to an algorithm book and, you know, look up how you solve that problem and find the, the right algorithm before starting to code. But there are lots of things that we have to do for which nobody is designed an algorithm. And so for those things, you need to stop and think, and that thinking needs to be done before you start coding. And the thinking is really independent of the coding process. The difference between when you’re thinking about bubble sot versus quick soar, uh, everything you’re thinking about applies no matter what language you’re you’re coding.

Leslie Lamport 00:28:14 Well, in addition to, uh, computational complexity, there are other, uh, important aspects of a design or an algorithm and particular simplicity. And just like, you’re not going to find the best algorithm in terms of computational complexity by, uh, coding. Similarly, you’re not going to come up with a simple design through any kind of coding techniques through any kind of programming language concepts. This time simplicity has to be achieved above the code level before you get to the point, which you worry about how you actually implement this thing in code. Now, when you’re writing a program or building a system, there are basically two problems that have to be solved. One is what should it do? And the second one is, how should it do it now in principle, these are completely separate ideas. One idea for sorting is what does it mean to sort while you take a particular list and you rearrange its elements so that they’re in increasing order. That’s the one that has nothing to do with the, how the, how is, are you using Quicksort or bubble sword or heap sword.

Leslie Lamport 00:29:45 Now those two concepts are not completely independent in the sense that, uh, you may, in principle, you could decide that you want to do something, uh, the wad, and then when it lbs the programming, it, you discover that, you know, you can’t, that is, you don’t know how or the, how is too expensive or something like that. So I don’t mean to imply that what you should first do is fake and that completely abstractly about, you know, what something is supposed to do. And then only then do you think about how you do it? And part of engineering is understanding web what you can do in practice and what you can, but given that caveat, you really should understand what the system is doing before you try to implement it. So they’re two separate things you want to specify about a program or a system, what it does and how it should do it.

Leslie Lamport 00:30:57 Sometimes it’s obvious it’s what something is supposed to do. Like you say, you want to sort a list. Well, that’s very straightforward. Uh, it doesn’t require a very complicated specification to describe it. Uh, other times, uh, the really hard part of something is to decide what it’s supposed to do. And it’s really important to understand what something is supposed to do before you start to do it. And very often, once you’ve decided precisely what something is supposed to do, implementing it, the coding, the how is quite trivial, and it hardly needs a specification at all, or it might be so simple that you, you really can just start coding without writing any precise description of how it does it of beyond the specification, what it’s supposed to do, or in other words, uh, how it’s supposed to do it is so obvious given what it’s supposed to do, that you may not need a specification of how,

Jeff Meyerson 00:32:10 And so the composition of this spec should, should this be done in maybe like iterative drafts as you’re thinking about the problem, because you say that, you know, in order to be actually thinking about a problem and you need to be writing, so is there, is there like some sort of stream of consciousness process that you go through before you sit down and say, okay, now I’m going into spec writing mode, or do you just sort of write a spec and then iterate on it and iterate on it, then move on to the program writing phase?

Leslie Lamport 00:32:43 Um, well, first of all, there are lots of different things that can go by the name of specification. Uh, and, you know, I use all of them. Sometimes a specification I write is a few English sentences. Sometimes it’s a very complicated, uh, mathematical description of, of the, the, the, of the object, either the white or the how, uh, it depends, you know, which one is appropriate, depends on the problem. You know, how hard the problem is, how important it is that it get done, that it get done correctly, uh, and various things like that. And it’s not like, well, anything you do, isn’t iterative process. Uh, you start by thinking about something and then you start writing it. And in the course of writing, you rewrite and you rewrite and you rewrite now a specification can be anything from a few English sentences to a completely formal mathematical description of what or how the program is supposed to do things. Um, I use all of them depends on how difficult the problem is and how important it is to let the program be correct. A lot of programs are I write just for my own use and I can live with bugs. And it’s not that important. That they’d be absolutely correct. And, but sometimes, uh, I write code for other people to use and I really want it to work. Right.

Jeff Meyerson 00:34:27 So at the end of the talk that you gave, someone asked a question about using UML to, to describe, um, systems and from the response that you gave. Um, I kinda got the impression that maybe you had some disdain for, um, for, you know, describing distributed systems in terms of boxes and arrows, and you suggested the use of predicates and next day relationships. And I’m curious whether the notation is really the issue, because like, it seems to me that boxes and arrows are essentially the same thing as predicates and next day relationship. So is it, is it just the usage of, of those two things?

Leslie Lamport 00:35:14 No. The important thing is not, you know, what, you’re, you know, the syntax of what new writing, uh, the important thing is the precision, the rigor that in order to understand things, you have to write them precisely. And I use mathematics because that is precise. Um, UML what I know. Uh, I know next to nothing about UML, but what I do know is the language was invented first, and then people came around and tried to give semantics to the language. Well, in other words, what that means is that the language was invented first and it really didn’t mean anything. Uh, and then later on, people came around to try to figure out what it meant. Well, that’s not the way to design a specification language. The importance of a specification language is to S is to specify something precisely. And therefore what you write the specification, you write has to have a precise, rigorous meaning.

Jeff Meyerson 00:36:27 So for people that, um, don’t have the, uh, I guess the mathematical chops to be able to write, um, according to the two, I guess the, the formalities of, um, you know, the, the predicate and next state relationships syntax, um, is, you know, is UML, uh, sort of an, an excusable, uh, next option, because I mean, it, you know, if it’s between, uh, you know, learning predicate next day, relationship syntax, and, um, and then when the, uh, the other option is, uh, sort of, you know, making a more sloppy spec, but then trying to write code and then hack it out from there. Um,

Leslie Lamport 00:37:17 Okay. You’re your whole set. Your whole question is based on false premise, you’re basically saying, well, you know, if people can’t think precisely, uh, should they just draw fuzzy pictures of boxes and arrows, right? Uh, well, people who are programmers, shouldn’t be able to take things precisely because you have to be able to think precisely to write code. And when you say they don’t have the mathematical chops, uh, that’s nonsense the mathematics that when you needs, in order to write specifications is a lot simpler than any programming language. Uh, it’s really, the mathematics you need is, is what you learn in a, uh, an undergraduate course on discrete math. Uh, basically first order logic, uh, sets and functions, what has to be learned is how you use that to specify software. And that, that takes some, some education that takes, um, some learning. Um, I have a mathematical language for doing that.

Leslie Lamport 00:38:39 It’s called TLA plus, uh, your listeners can, uh, find it on the web and just go to my homepage. And there’s a link. I think it’s called to the TLA webpage or something like that. And they’ll find, um, there’s a hyper book, hyper textbook, which is the best way to start learning it. But as someone who said, this is not, uh, uh, rocket surgery, this is really simple. Uh, unfortunately, uh, mathematical education, uh, at least in this country is such that it tends to make people frightened of math, but anyone who can write C code, no, should have no trouble understanding simple math because C code is a hell of a lot more complicated than, than simple math. And again, the important thing is not so much the language. I mean, I use math, there are other, uh, specification languages that, um, the better fine, the important thing is thinking precisely the benefit of using math is that it teaches you to think rigorously, to think precisely. And the important point is the precise thinking. And so what you need to avoid at all costs is any language, that’s all syntax and no semantics, because that is not going to get you to think rigorously. That’s going to get you to fool yourself into thinking that you’re, that you’re thinking,

Jeff Meyerson 00:40:21 Just start to cap things off. Um, how has your thinking about distributed systems changed since you started working on the subject? And I guess since, um, since distributed systems have become, um, more and more, uh, necessary for the average programmer to understand and work with,

Leslie Lamport 00:40:44 Well, I’m not sure exactly what you mean by how has my thinking changed. I mean, my basic mode of thinking hasn’t changed, it’s basically the idea that I want to understand things and understand things for me being means being able to describe them mathematically, uh, I’ve worked.

Jeff Meyerson 00:41:07 Yeah, I guess what I mean is, um, have, has the landscape changed such that new situations and, um, problems have developed that have, um, expose you to things that you, uh, hadn’t tackled before?

Leslie Lamport 00:41:27 Oh, man, the world has changed and honestly, and new problems come up, uh, that are interesting. There’s been a, not an enormous amount of theoretical work, uh, that is in algorithms and theory that’s been done on distributed systems. Unfortunately, I can’t really give you a very good answer on that because, uh, I do very little work on distributed systems these days. And I haven’t for about a dozen years, I dabbled a little bit mostly because, uh, I have friends and colleagues who are interested and they will get me thinking about something, but most of my work has been on, uh, specification and verification.

Jeff Meyerson 00:42:15 Do you see yourself moving back into that field at all in the future and maybe working on them again?

Leslie Lamport 00:42:22 Um, I think it’s unlikely. Um, I’ve now 73 years old and I don’t have, uh, that much of, uh, of my career ahead of me. So, uh, you know, at least for now I’m thinking of really continuing and trying to, to in some sense, finish up, uh, the, what I’ve been doing on specification.

Jeff Meyerson 00:42:47 Sure. And so I guess I have one more, um, question. Um, so I’m kind of curious about this, um, in, in the realm of thinking for programmers, this wasn’t exactly in the scope of your discussion, but I feel like it’s, it’s important for we’re thinking for programmers. How do you build the mental resolve to work through a problem? I mean, maybe this isn’t something that you had an issue with, but is there, is there some sort of like courage or persistence or emotional characteristic that defines a programmer who is able to systematically break down a problem?

Leslie Lamport 00:43:29 Well, I think I’ve had it easy, much easier than programmers have it because I’ve been in environment in an environment where I don’t have hard deadlines where I’m given the freedom to explore problems that I think are interesting and important programmers are in a much more difficult situation. They have a specific task to perform and they have to get it done in a reasonable amount of time. Now, what I’m advocated for programmers is what I do myself, everything I say about writing specification, you could look at code I’ve written and you will see that most of the code, there are more comments, documentation, and specification of the code than there is code itself. And I do it because that produces a better program in less time. But it does that for me because I’ve been doing it for a long time. And I know how now a programmer who has never done this before never tried writing specifications before. It’s really hard for him or her to sit down and do it in the context of his or her current job.

Leslie Lamport 00:45:05 It takes will not say willpower. Isn’t the, isn’t the word. It’s a incentive to learn how to write specifications. And it’s essentially it has to be done in a most programmers in their spare time before they get to the point where they can actually apply it and use it in practice. There’s an article that has been written by, uh, a group of people at Amazon. And I believe will be appear one of these months in communications of the ACM. Although I believe that it has the final acceptance has not been given yet, but I expect that it will appear and they will. That paper describes how TLA plus my specification language came to be used in a group or among several groups, uh, at Amazon. And I think that will give an idea of what it takes for this new idea of specification to take hold.

Leslie Lamport 00:46:27 It requires someone with persistence and foresight to believe that this can be a solution to their problems. And it takes engineers and their managers who are willing to invest the time and effort to use it because they believe that it will give better results. And in the Amazon case that has paid off for them. But when a programmer doesn’t have something like that to point to as something that works in his own problem domain in his own context, then it takes a yeah, it takes courage, uh, for a programmer to start doing that and to give it a try and to really try to make use of it and can really try to do things better than he or she is now doing them. And that takes courage for

Leslie Lamport 00:47:31 An ordinary programmer. It didn’t take courage for me.

Jeff Meyerson 00:47:35 Okay. That’s, that’s a great response. I really appreciate it. Okay. Well, uh, Leslie Lamport thank you for coming on to software engineering radio and, um, giving an excellent and informative interview. Thank you. Leslie can be reached through his website lamport.org in the show notes. You can find links to some of his papers, as well as the talk I referred to in this episode, thinking for programmers. Thanks for listening to software engineering radio. We want to know what you think. Go to iTunes and read review of the show, stating your opinions. It would help us improve the show. Thanks.

[End of Audio]

This transcript was automatically generated. To suggest improvements in the text, please contact [email protected].