Featuring
Sponsors
Tailscale – Simple, secure networks for teams of any scale. Built on WireGuard.
Sentry – Watch Lazar Nikolov livestream on YouTube at youtube.com/@nikolovlazar. Use the code CHANGELOGMEDIA and get the team plan FREE for six (6) months.
Notes & Links
Chapters
Transcript
Click here to listen along while you enjoy the transcript. 🎧
Alright, I’m here with Leslie Lamport, a distinguished scientist at Microsoft Research, creator of LaTeX; not the
rubbery substance, but the documentation system that you’ve probably heard of or used. It’s used in Academia, it’s used in scientific circles, math circles… And a Turing Award winner. Leslie, thanks so much for coming on the show.
Thank you. You might want to try that again and pronounce it either LayTech or LaTec.
Ah, I was reading about this controversy, the pronunciation controversy. So as a layman, I see L-A-T-E-X and I do think of that rubbery substance. But the initial author – it was Tech, right? It was supposed to be T-E-C-H was the sound… And your take on that is LaTech. That’s how I should say it?
Alright. Now, where do we get Tech out of Tex? That’s the curious bit.
Oh, that’s because LaTeX is built on top of Don Knuth’s tech typesetting program.
Okay. And Knuth called it Tech, even though it was Tex, is that right?
Yeah. He says it’s the Greek pronunciation of the original word. Not speaking Greek, I wouldn’t know.
Ah… Well, you seem to have some Greek influence, though. Paxos… A lot on Greek mythology going on. Is that an interest of yours?
No. It was just – well, for the Paxos paper it was just something that seemed a good idea at the time. Before I get away from that, I should say that Knuth did all the heavy lifting in building Tex. That was a real remarkable thing that he did. What I did was, in comparison, quite simple… Just building a macro package on top of it.
I see. So Knuth did all the heavylifting… However, in terms of the tooling, it’s still used, it’s still prominent. Is it still the majority tool that is used in those communities for specifications and writing? Or is there something that’s usurped it since?
No, but I think it’s still math and physics… At least it’s still the standard – I don’t know about other fields; some fields, it is. Some fields – I’m sure chemists have never heard of it.
Right. Well, as a working software developer, I’ve definitely heard of it. I don’t know it well enough to pronounce it correctly, as you can tell… But I hear it talked about often. Some people love it, other people use it in anger, but everyone seems to use it. It still seems to be the best. And to me, what speaks to me about it is the separation of what you’re saying versus how it looks. That’s a key aspect, right?
Oh yeah, that was why Tex needed something on top of it.
You know, Knuth intended for things to be built on top of it, but I’m not sure he expected so much of the underlying tech to be hidden from the user. By the way, I should say that the whole idea of basically separating the ideas from the typesetting – that was done by Brian Reid in his scribe system. When I started, I used Scribe, and it seemed perfectly obvious to me that was the thing to do.
[08:08] One of my failings in my career is building on things that seem natural, some seem obvious to me, and without realizing that they were new ideas, and that they were significant ideas. I think a prime example of that is in my Time, Clocks paper, where it was inspired by a paper that I read from Paul Johnson and Robert Thomas, where they had an algorithm for something, and I realized that their algorithm wasn’t quite the right one, because it basically violated causality. We could have something that calls something else, but things were ordered as if they happened in the opposite direction.
So one of the two significant contributions of that paper was pointing out what this notion of causality – which again, seemed very straight, very obvious to me… But what they had done – they had used timestamps, they added timestamps to the messages. And I just assumed that that was a well known idea, that people did that, and sort of not even worth mentioning… But as it turns out, I think they were actually the first people who did that, because their paper is not very well known, and mine was. People have credited me with inventing/adding timestamps to messages.
Ah… So a couple of themes here, the first one being is you building on the work of other people who have come before, and maybe getting in some sense some of the credit on accident. Deflecting, as I can tell… But also, this idea of your ideas, which you’ve put into papers, and have been read now, and implemented around the world, seeming obvious to you, but not necessarily to the rest of us, right? Do you find it hard to explain your ideas to people, or to bring them along with you?
Yeah. Because I just expect more of them than it’s reasonable to expect of most people. Fortunately, I’ve had some really smart colleagues who were smarter than me, in fact… And I think if I’ve been more successful than them, I think it’s because of my different way of looking at things, not by being brighter than them. So I’m not a genius; I’m not in the league with people like Einstein, or Feynman, or I could name any number of people.
If we were to focus in on the looking at things differently than other people… Can you describe that, what your angle is, or how you see the world that’s eschew, or that’s tangential to maybe the way your colleagues were looking at things? What’s that different perspective?
Well, it’s very simple actually to explain why I’m different from most computer people – it’s because I think like a mathematician, and I approach things mathematically, not computationally.
Can you give a for instance, like maybe in a basic case of a situation where maybe me as a programmer would approach something imperatively, or computationally, step by step, whatever it is, and you as a mathematician, maybe you would look at it differently? Because I can’t look at it your way; I want to. And so how do you look at things – when you say “I think about it in math”, to me, I’m just like “You’re gonna add numbers together?” What do you mean exactly?
[11:59] Yeah, it’s funny, I don’t have a ready example, except something that happened fairly recently with a colleague. He asked me how would I define something. And he said he found it really hard to write this definition. And it was defining some property of sequences; of actually infinite sequences. And it seemed really easy to me, so I wrote the definition. And what blew his mind was that it was like a recursive definition just like he was trying to do, that is you define it for one, and then N=1, so what we get for N=1, define it for N=n+1. But the value that you’ve assigned to a given N, the value assigned to the N+1 depends on the complete rest of the sequences, infinitely far past N+1. And that’s perfectly obvious to a mathematician. But because he’s what I call trapped inside the box of computational thinking, that never occurred to him, because you can’t compute something by looking infinitely far ahead to find the next value.
Right. That’s where I’m sitting right now.
But he wasn’t trying to compute it, he was trying to write a definition.
A definition of the problem, or of a solution?
No, just the definition of some property of infinite sequences that he wanted to define.
He was a theoretician. This is theoretical computer science, in some sense. It’s talking about a few properties of programs, rather than how to write programs. So you represent the execution of a sequence as an infinite sequence of either states or steps, depending on how you want to do it… And then you can talk about programs scientifically by talking about those sequences mathematically.
Gotcha. So this kind of is a pattern, or at least echoes what we talked about earlier with Knuth’s Tex, and subsequently LaTeX was the separation of concerns. In that case, it’s from the ideas, and then the display of the ideas, of the typesetting. You’re talking about separation of concerns. You’re talking about specifying the ideas as separate from the implementation. When you say “programming”, I know in the Quanta video, which we’ll link up in the show notes as well, that featured you, you made a distinction between coding and programming. This idea that, okay, there’s the idea that you’re trying to express… Because what good is a program if it doesn’t do something, or express something, or change the world somehow, or provide some sort of value? So you have the idea, and then you have the implementation. And many of us – and I hold myself in this category – they’re kind of munged together, and kind of like grow out of the same milieu. But the way you look at it, the idea, the program is a separate thing altogether from the implementation. Is that correct? Am I thinking about it the way that you think about it?
Well, yes, exactly. I mean, I wouldn’t say it’s separate –
Well, one informs the other.
Well, the thing I like to say is coding is to programming what typing is to writing. I mean, obviously, it’s somewhat hyperbolic, because there’s a lot more intellectual effort goes into coding than typing… But I think, actually, maybe before the days of computers the analogy would be writing, and typography. Typography is an art. A lot of effort goes into designing a book. But that’s completely separate from the writing of the book, the ideas and that what the book is trying to express. But it’s not completely separate, because good typography will reinforce the ideas. So in the coding, programming aspect of it, you can think about what the program is going to do without an understanding of whether you can code it or not, or how you can code it. So the designer of the program has to understand what you can do with code.
[16:30] Actually, there are two things that you should do before you start writing code. The first one is figure out, decide what the program is supposed to do. And again, you can think of that in terms of what you have to tell the user of the program, what the program is supposed to do. Now, that program very often is code to be used by somebody else in his program, or her program… And I have a very simple criterion for whether you’ve done this properly, is that you should write this description of what the program is supposed to do in such a way that someone can use it without having to look at the code. Then the idea that I can be able to give you something that’s a bunch of code, and you should be able to use it without having to look at the code is foreign to programmers. It’s completely obvious to me, and I think it’s completely obvious to a lot of software engineers, but it doesn’t seem to be obvious to programmers, because they’re not programmers, they’re coders. And if all you think you’re doing is writing code – well, of course, somebody has to read your code to understand what the code does. But that’s at the heart of so much of what’s wrong with software being built today.
So you’re referring to like a formal specification.
It doesn’t have to be formal.
Well, it has to be usable without the code. You can do that informally?
Well, by formally I mean writing it down in mathematics, or in a language like TLA+.
That would be formal in my mind, yeah.
I mean, I do this whenever I – if I have a coding class, and some method in this class, I will write a description of what that method does. And in 95% of the cases, it’s just English;, just pure prose.
Maybe a formula or two tossed in. Occasionally, pseudocode. Usually not, but sometimes perhaps pseudocode.
Whatever works. But it has to be precise enough that somebody can use the code without having to read it. And if what it does is simple enough, that you can explain it in English, that’s great. Occasionally, there’s a piece of code that – but you have to start writing it. And when you write it, you should be able to see whether what you write – you know, as you write it, you’ll know whether what you’re writing is making sense. If you want to understand something, you’ve got to write it.
There’s this cartoonist [unintelligible 00:19:14.18] has this wonderful caption of a cartoon, which is “Writing is nature’s way of showing you how fussy your thinking is.”
I had this one example, this one certain aspect of actually writing a parser for TLA+ that somebody was doing, and he sort of asked “How you compute this little condition of some check of correctness of the specification?” And I thought, “Oh, well, this is quite simple. I would write down a piece of – as usual, informal English, a little math…” And the more I started writing, the more tricky I realized it was. And I decided that I needed to write a TLA+ specification of it. Fortunately, the person who was doing the compiler knew TLA+, so I didn’t have to explain the TLA+ to him.
[20:10] And he coded it from the TLA+. And I actually sort of asked him about that… You know, TLA+ is a lot different from Java, what he was coding it in. How much effort was that? And he said, “Oh, no, it’s really straightforward.” And actually, at some
