
Picture Me Coding
Picture Me Coding is a music podcast about software. Each week your hosts Erik Aker and Mike Mull take on topics in the software world and they are sometimes joined by guests from other fields who arrive with their own burning questions about technology.
Email us at: podcast@picturemecoding.com
Patreon: https://patreon.com/PictureMeCoding
You can also pick up a Picture Me Coding shirt, mug, or stickers at our Threadless shop: https://picturemecoding.threadless.com/designs
Logo and artwork by Jon Whitmire - https://www.whitmirejon.com/
Picture Me Coding
Leslie Lamport and the Free Software Movement
In this SCaLE wrap-up Mike and Erik discuss the final day of the conference and talks by Denver Gingerich called "What happens when hardware puts software freedom first? We built a router to find out" and Leslie Lamport titled "Coding isn't Programming", and we got to meet Leslie Lamport and take photos with him and give him Picture Me Coding stickers.
Music from #Uppbeat (free for Creators!):
https://uppbeat.io/t/night-drift/the-horseman
Music from #Uppbeat (free for Creators!):
https://uppbeat.io/t/night-drift/x
Music from #Uppbeat (free for Creators!):
https://uppbeat.io/t/qube/play
Erik
Hello, welcome to Picture Me Coding with Eric Aker and Mike Mull. Good morning, Mike, my friend.
Mike
Good morning.
Erik
Mike, I want to do something surprising for you. I would like to read you a short Walt Whitman poem. Is that really dorky and weird, me reading you a Walt Whitman poem?
Mike
It's a very dead poet society of you, but yes.
Erik
I don't want to be dead poet. I don't want to be in the dead poet society. I want to read you this poem. The poem is called A Noiseless Patient Spider by Walt Whitman. Here's how it goes. A noiseless patient spider, I marked where on a little promontory it stood isolated, marked how to explore the vacant vast surrounding. It launched forth filament, filament, filament out of itself, ever unreeling them, ever tirelessly speeding them. And you, oh my soul, where you stand, surrounded, detached, in measureless oceans of space, ceaselessly musing, venturing, throwing, seeking the spheres to connect them. Till the bridge you will need be formed, till the ductile anchor hold, till the gossamer thread you fling catch somewhere. Oh, my soul. Do you know this poem?
Mike
Actually, that's not a Whitman poem that I recognize. I don't think I know it. Is it in Leaves of Grass, I would assume?
Erik
I don't think so, no. I think it's pre-Leaves of Grass. Actually, I don't know when he published this. Here's why I wanted to read you this poem, A Noiseless Patient Spider. I always liked it. This is the reaching mind. It's like I want to connect things. I'm in measureless oceans of space. This is the world of ideas, the world of abstraction. I want to link things together. But there's this line, and you, oh my soul, where you stand. Sometimes I listen to a piece of music, and it hits me in the chest, and it feels like a salve for my soul. And I think, and you, oh my soul, where you stand. And that happened to me over the last few weeks. I've listened to this record you told me about, Patterson Hood. It's called Exploding Trees and Airplane Screams. Patterson Hood, the Drive-By Truckers guy. You told me about this record. What did you think of it?
Mike
I clearly did not love it as much as you do. I think to a certain extent I was kind of expecting another Drive-By Truckers record. which it is not.
Erik
Yeah, it's not, yeah.
Mike
There's some good stuff. It's just, it's not my expectation and the collaboration he did on this record with Waxahatchee is just an okay song, I think, in my opinion. Something
Erik
happened to me at the beginning of this year. I was listening to Spotify and they were like, oh, you like Jason Isabel. You'd probably like the last song on the Dirty South. And I was like, whoa, I don't remember this. I kind of gave short shrift to drive-by truckers 20 years ago when Decoration Day and the Dirty South came out. And somehow I fell in this hole and I was like, wow, I really, really love these records. They are great records, Decoration Day and the Dirty South. I rediscovered them. And then you told me about this Patterson Hood album. And I really like this record too. It's got this sad old guy air to it, but I'm enjoying it. His voice is not great, but there's this authenticity. I think my favorite song is this cheesy song on it called The Forks of Cypress. It's a nice, sweet, gentle love song. I totally understand not being enamored of it. It's kind of goofy and honest, but I love this song so much, and it made me think of the Walt Whitman poem. It feels like a salve for my soul when I listen to it. Like, it's healing me a little bit hearing this music.
Mike
I get that. I love those Drive-By Truckers albums, and I like the earlier ones too. And, you know, I think they have probably the best album title in the history of rock music with pizza deliverance. It's kind of a Southern joke. If you haven't seen the movie Deliverance, maybe it doesn't make that much sense.
Erik
I've never seen the movie, but I know the stories. His voice is not great, but it's
Mike
pure
Erik
and authentic. There's something there. What about you? You listened to music last
Mike
week? Yeah, I was listening to a very similar album. Cool. It's called Retromorphosis by the band Retromorphosis.
Erik
Oh. Also soul healing music, like a nice paste or butter you just spread on your soul to feel better.
Mike
It does something to one's soul, yes. I'm not sure healing is the intent.
Erik
Oh, different kind of. Got it.
Mike
It's a death metal album. I think what they call technical death metal because it's sort
Erik
TCP, networking stack, it's pretty technical. Death metal album.
Mike
Not exactly,
Erik
but... Okay.
Mike
Yeah, the album I've been listening to leading up to the conference and during the conference was Retromorphosis, which is a pretty straight death metal album. It's kind of like my favorite thing to put on my noise-canceling headphones and listen to and read the 15,000-page ARM technical architecture manual.
Erik
What you're reading and what you're listening to sound to me like you're putting a big sign on your door that says, go away. I'm reading about arm architecture and I'm listening to death metal. These sound like anti-social activities to me, Mike.
Mike
Yeah, it's kind of a, I don't know, like a porcupine sort of thing.
Erik
Mike, last week we were at the SCALE conference, SCALE 22X. It's the 22nd edition of SCALE, even though this is 2025. Something that people kept being confused about, SCALE 22X in 2025. I want to talk about that. I want to reflect on what it was like going to a conference together, what we saw and what we experienced there. Before we do that, though, I do want to say, friends, if you are enjoying the show and you would like to support what we're doing, we now offer Patreon memberships starting at the $4 level. For only $4 a month, the cost of a cup of coffee for Mike and I, you can sponsor our show, help us deliver content to your digital door once a week for the rest of the year. We like running an ad-free show, don't we, Mike? You like that?
Mike
I love it.
Erik
I like it. I honestly do like it. Maybe that's my Linux spirit shining through. I like running an ad-free show, but we do rely on our Patreon sponsors to help cover the cost of the show. So if you're enjoying our content, please consider becoming a Patreon sponsor. In a show of thanks, we'll read your name aloud on this show. And we're also going to have some other cool perks in the future. Stay tuned. We do want to mention our two latest Patreon sponsors, Frank Holland and Irina Talyakova. Thank you so much for sponsoring our show. We appreciate your support.
Mike
Also, please, please, please check us out on Blue Sky. It's really the only social media that we are using at this point in time. And we definitely need more followers.
Erik
So today I wanted to wrap up and reflect on the Scale Conference. It's been a week since you and I were in Pasadena. We were drinking coffee. We were conferencing our hearts out. We didn't get a chance to talk about that last day of the conference. It was a cool place to be. I haven't been to a conference in years, and I quite appreciated being there.
Mike
Yeah, it's an interesting crowd, very diverse and kind of little subcultures of the Linux world.
Erik
Yeah, that was rad. And it put me in mind of feeling like, wow, I should go to more conferences. It's fun going to conferences and talking to people. I end up just wandering the hallways and meeting people and talking about stuff. One guy in the elevator was like, well, that's a cool watch. What's your watch? And then we got into this whole like watches conversation. I'm not like a big watch guy. Or you put on your headphones and listen to death metal.
Mike
You know, whatever you choose.
Erik
Yeah, big arm manual in front of you like go away. I'm listening to death metal and reading about the arm architecture. sure so on sunday we went to the opening keynote by a person named denver gingrich the name of that keynote was, what happens when hardware puts software freedom first? We built a router to find out. Denver Gingrich is the Director of Compliance at the Software Freedom Conservancy. This is a nonprofit. They fight for free and open source software. This is how they describe what they do, their mission on their website. Our mission is to ensure the right to repair, improve, and reinstall software. We promote and defend these rights through fostering free and open source software, projects, driving initiatives that actively make technology more inclusive and advancing policy strategies that defend FOSS. Gingrich started by saying, why are we here at this conference? And he answered this question by saying, we probably want to find out about cool technology, but we're also here to be empowered. Technology is empowering and shifts in technology are empowering for different groups. This reminded me a little bit of the talk by Hazel Weekly. I'd gone to the day before. Talking about software licenses, talking about power, there's a political philosophy on the surface here. For example, what he had in mind, Gingrich then brought up the OpenWRT1 router. This is an actual product. You can buy it. It's $89, and it has open source router software installed on it, and the router itself is modifiable. You can open it up and change it. This is the router that they used all throughout the conference. It was sponsored by the Software Freedom Conservancy. And he contrasted this with like fancy routers on the market for more than 400 bucks. I think he gave the example of an Asus router. He said, here's a router, cost $400. After four years, they end of life the thing. They didn't want to put any more updates to the software on the router. And that kind of sucks. It'd be much nicer to be able to keep old routers out of the landfill by just putting open source software on them. And then he moved on to talk about all these lawsuits that are sponsored by the Software Freedom Conservancy against corporations shipping closed source or proprietary software on top of Linux. This is in violation of the license of Linux, which is a GPL license. So Gingrich is like, we are out here fighting for your rights. Linux is licensed under the GPL. That's what we call a copy left license. This is how they define copy left licenses. They say these are licenses, software licenses, that have the intent to promote sharing. The intention is for this to be achieved by granting everyone the same exact rights, permissions, privileges to modify, improve, and include the software in their products. Did you understand this argument? Did this make sense to you, what he was saying?
Mike
I think so, yeah. I mean, he talked a lot about these suits that they filed or the requests that they've made to these companies to have them send their software or make their software available. I think it's a laudable pursuit. There's a part of me that thinks that some of these devices really shouldn't have software in them at all.
Erik
Like what?
Mike
What example? Well, I talked about getting a source code for TV manufacturers. I confess I have a Samsung TV. I don't really want to see the source code for my Samsung TV. I guess I'm glad that there are people out there with the ideals to pursue that. But I really want my TV not to have software in it. I don't want it to spy on me or recommend me things. I have a computer for that. But the smart TV, not
Erik
a bad thing to have because you can automatically connect to all these content providers, Netflixes and Hulus and others, right? So it's kind of cool that the TV can just log in and do that. But you're right, if it's proprietary, they're going to put all kinds of software inside to kind of piggyback on your activity to watch and see what you're doing and then probably sell that back to other people for advertising or market research or whatever. On the one hand, it's nice to have the functionality, but on the other, when it's this closed system, it comes with some maybe dark or shadowy activity. And Gingrich's argument is, hey, they're building this stuff on top of Linux, which means you have a right to see what's in there. You have a right to modify it. You have a right to repair it if it stops working because they decided to stop shipping software updates.
Mike
Yeah. And I also think there's, he talked a lot about in the course of building their router, the sorts of things the manufacturers do to sort of meet the letter of the law, but defy the spirit of it. The software Freedom Conservancy asks for software and they send them, you know, partial software, but not something that they could actually modify. or
Erik
the
Mike
manufacturers say that they make a serial port available, but to get to that serial port, you have to take the box apart and solder things. So it does make me happy that there's somebody out there trying to hold them to the things that they have sort of implicitly agreed to, but I also sort of don't get nearly as excited about it as they do, I think.
Erik
Yeah, I think I'm the same. he he said that the software that became open wrt that router software it was open source as a result of a lawsuit there's an idealism here and that idealism it has i have to confess like a little bit of nostalgia for me it takes me back to the warm and exciting 20 years ago when i was first getting into linux and to be a member of the linux community meant that you were a lot closer to these ideas. You had to actively go out of your way to adopt Linux in those early days. You had to work hard. It took effort. But that's not the same these days, I don't think.
Mike
I don't know. Like this router that they built seems like a pretty good router. You know, it has the features that they were looking for and it's relatively inexpensive, but it's not clear to me that, you know, I don't really want to assemble my own router. probably I'm not going to tinker with my own router. So as I said, I really like the philosophy, but I don't have the same fire in my belly that these young folks do to do things this way.
Erik
Yeah, I wonder if you go in that direction. Your router becomes not just a router, but also a hobby. Do you want your router to be a hobby? In the early days of Linux, for me anyway, where I was constantly like putting different distros on and configuring them and playing with them and comparing things, I got to a point eventually where I was like, oh, I really don't care that much. I just want to spin up the operating system and then just start working. It became less interesting as a hobby because I wanted to do stuff on top of the computer. I think there's something else that's kind of surprising here. If you take Linux, arguably the most successful computer OS operating system in history, if you were to tell people there's this idealistic political philosophy under the surface, I bet most people would go, huh? The analogy for me is if you walked into a hardware store, you hung out in the power tool section, and every time someone picked up a particular power drill, you walked up to that person and you marched up to them and you said, hey, did you know there's an ethos inspiring the work on this power drill? The people who produce it want you to be free to repair, modify, or extend it. But if you make any money on your modifications or extensions to the power drill, you have to promise to give those modifications back to the community for free. I think people would be like, what are you even talking about?
Mike
Yeah. It's one of these turtles all the way down sort of situations. I don't want to get too philosophical here, but I agree with the right to repair laws and stuff like that. But, you know, there's so much about modern computers that I just have no control over. Even if you're buying like a Linux laptop from System76 or something like that, there's just so much on there that is really out of your control. So it's just kind of like where does the interest stop? You know, like most consumers when they buy a computer probably never want to mess with it other than maybe like changing their background or changing some settings. You
Speaker 3
know,
Mike
I'm the sort of person who likes writing assembly language and trying to figure out stuff about my computer, but I'm never going to actually like go in and solder a new resistor or something.
Erik
I think the power drill analogy is a funny encapsulation of how this idealism sometimes feels to me. Most people I think would be like, I just need a drill to fix something in my house. It's like this toolness, right? I care about it as a tool. It feels in that way politically neutral. if you said to someone using the tool we are fighting for your rights as a tool user i think a lot of people would be confused like what on the other hand i bet almost everyone would be like oh yeah cool like i could fix this myself i don't have to pay someone to fix it that sounds rad so there's this pervasive culture that seems out of square with the reality we're used to buying tools we're not used to thinking about our rights with respect to the usage of the tool and I think that the idealism is out of step a little bit with the reality which is not a critique of it it's not that it's wrong it's just that I hear it and I'm like wow these people this is great I'm glad they're here this is cool I buy what they're saying
Mike
are they in the same operating
Erik
the same world
Mike
I am I feel like the idealism is probably necessary to a certain extent maybe there's even a different word I want here. But in any case, the sort of absolutism about this stuff, I think it may be necessary to a certain extent because my cynical take is that the manufacturers will do whatever they can to make you buy more of their stuff.
Erik
Yeah. And built-in obsolescence is pernicious. Yeah.
Mike
If there's money to be made on spying on you, they will do it. If there's money to be made on collecting your data, they will do it. If there's money to be made on bricking your device after four years, they will do it.
Speaker 3
And
Mike
so I think the sort of crusader attitude that you see from these organizations is probably a necessary thing.
Erik
Yeah, I'm with you. So that was a keynote. That's how the day started for us. That view, that perspective was present in parts of what I saw at the conference. The other perspective I encountered a lot was, hey, let's go deep into things you're using let's try to teach you more about them whether it's docker or git for me or networking there were a lot of there was this whole nix track i hung out with rob a lot after the keynote i met a guy named eric reiner he works on a project called vorpal and eric introduced me to tom breckney who's a lead engineer at flox dev and also a lead on the nix project so that a lot of the people including rob and eric they were big fans of nix people running the conference and Eric's project Vorpal is a reimplementation of Nix but the idea is you can bring your own configuration language or programming language Nix is an operating system, a programming language and a package manager and that's kind of a large pill to swallow for a lot of people do I want all of those? Do I just want one? Nix of course gets you repeatable builds so they're deterministic builds you can build the exact same thing every time and you can cache chunks of the build so you can build very rapidly. Eric actually, interestingly, he livestreams development of his project, Morple, on Twitch. What talks did you go to on that last day,
Mike
Mike? So other than the two keynotes, one of which we've already talked about, the only other technical session that I went to was a super esoteric one called Bringing Per-CPU Variables to Rust for Linux.
Erik
Jeez. That's so esoteric that I'm like, do I want to know?
Mike
I was given by this young guy named Mitchell Levy, who I think is at Microsoft. The idea here is that Linux supports something called per CPU variables. Normally, you know, this is a kernel thing. And normally you would, to attempt to do this, you would be doing it in C. And the basic idea behind per CPU variables is that you can implement certain things like counters, maybe. that are keeping track of something per CPU core, and it makes things much faster at a very small-scale level because you don't have to worry about things locking that memory to make memory accesses for that variable
Erik
atomic. So atomic increment, for example, you don't have to worry about that. It's just right there in that CPU. That's right. So, you know, if you have this situation
Mike
where you want to track something on a per CPU basis, you can do it with these per CPU variables. And I guess it's not a common feature in Linux. You know, again, it's a kernel level thing. But there are some difficulties in doing this in Rust. And so this guy, as part of the Rust for Linux project, has been trying to get to the point where they can do this in Rust. And I think also the idea is you might be able to do it in user space
Erik
in
Mike
Rust programs. But there's some trickiness to doing it in Rust. And so his talk is basically about how he's been going around about trying to bring this feature to Rust and the difficulties involved. And it's still a work in progress. It was a very interesting talk, but obviously a pretty narrow audience.
Erik
Yeah. What did you get out of a talk like that? Do you think you might use the information you got in there somehow? I just,
Mike
I had
Erik
two motivations.
Mike
One is I thought I might learn some stuff about Rust, maybe did a little bit, but also I was just kind of interested in the CPU level architecture that's involved in doing these things.
Speaker 3
I mean, he's doing
Mike
it, he's doing it specifically for a 64-bit x86. So it's, you know, it's the sort of thing where you probably have to do slight re-implementations for every new processor architecture. It was, for all practical purposes, kind of like a kernel talk.
Erik
Wow. It sounds interesting from afar. That's what I want to say.
Mike
Yeah, it was interesting to its very narrow audience, but probably not something we will be doing a future episode about.
Erik
Narrow audience. How many people do you think attended that talk?
Mike
There were probably 20, 25, I think. pretty exclusively people doing kernel work and embedded work, that type of thing.
Erik
So at the end of the day, the real draw for us, one of the reasons I wanted to go, and I imagine you wanted to go too, is to see Leslie Lamport speak. I've never seen Leslie Lamport speak.
Mike
Yeah, this is the first time I've ever seen him in person as well.
Erik
He's 84. He said as part of his talk that he started writing, he started programming in 1957.
Mike
That's even before me.
Erik
We sat down probably second or third row for the closing keynote. This was the very last talk before the conference completely ended. There were people behind us who it didn't seem like they'd ever heard of him. I don't know if this is representative of the crowd. I imagine a lot of people there knew who he was. But the people behind us were like, whoa. On his first slide, it's Leslie Lampor, Microsoft Research. They were like, this guy's with Microsoft. He's going to tell us about why we have to care about Windows and Microsoft products. And I was like, wow, I'm in a different crowd. That's obviously not. And his talk, coding is a programming. There wasn't really anything too surprising in there. We could summarize it. hear, but did you know what he was going to say before he started?
Mike
Not exactly. I guess we should probably say for the benefit of people who haven't listened to all of our previous episodes in which we mentioned Leslie Lamport, about a third of them. So he's probably most famous for his work in distributed systems. So I guess I went into it with kind of the expectation that he would be talking about something related to distributed systems. He's notable for several significant developments in that field. And so I thought he would probably talk about something like that. And I guess in a way he did because he did bring in TLA Plus eventually. I don't think there was anything too surprising about his talk. I think it's stuff we've heard from him before, but it was definitely not as focused on distribution. systems as one might have expected.
Erik
Yeah. He offered this argument that he's been making pieces of for over the last 20 years, I think. And he makes this argument most fluently in a book called A Science of Concurrent Programming. And this is a PDF you can find on his website for free. So over the course of about 45 minutes, he put together this argument that roughly works like this. He says, programmers care too much about programming languages or hacking or coding. And he's a little bit dismissive of coding, in quotes here. Instead, he said programmers should care a lot more about algorithms. But to validate the correctness of their algorithms, they should rely on mathematics. And Lamport's always like, I come from a math background. Programmers are afraid of math. You should use math. So to validate correctness of algorithms, we should rely on math. But that might sound scary. But for him, the math in this case actually means we should write and validate abstract programs. So an abstract program is where most of your real-world concerns have been stripped away. There's no network calls. There's no talking to the database. You don't even have clocks in most cases. You don't even have like, well, now it's been a second sleep type of stuff. An abstract program is not a program you could use to solve the actual program you have, but it's actually like a model of your program, or it's an interpretation. of your program. And so he used a lot of terminology he's been using over the last 20 years to talk about abstract programs in TLA+. He says an abstract program is roughly a sequence of states. A state is an assignment of a variable. And a step is a transition from one state to the next. And finally, a behavior is how the program functions, what it does. So we're trying to validate the behavior. It's a sequence of states. And he says, programmers are taught to code. They're not taught to abstract. He did say something that was a little bit almost alarming for me to hear. He said at one point, maybe TLA plus is not something all programmers will be able to understand. I wrote that down, but it's sort of scary to hear that.
Mike
I am unsure about that, but I suppose that in a broad way, there are people who do various professions who probably can't do the most complicated thing in their profession across the board.
Erik
I want to buy that TLA Plus is not the most complicated thing in the profession, though, but I do find it hard. I do find it difficult. After he got through this talk, he was like, I could take questions or I can give you another short talk. and he asked the audience to vote and we all voted for the next short talk. And the next short talk was called Why Programs Should Have Bugs. So he said that over his career, he's seen we've gotten more and more complex programs. They're based on libraries. Things have gotten harder to use as we built upon these layers of complexity. He said a program can only have bugs if there's a precise description of what it should do. That was an interesting, more formal idea of a bug for me. You can only say a program has a bug if you know for sure precisely what the program is supposed to do and how the bug really conflicts with that behavior. But he says very few programs have a precise description of what they should do. And so should we even bother giving a precise description to our programs? And he's arguing again, we should. We should build abstract programs which describe and validate the behavior. So very much focused on programmers care too much about programming languages. He wrote at one point on the screen, stop caring about programming languages. Stop caring about coding. Use abstract programs to validate algorithms. When it came time for questions, someone asked him if he saw more people using tools like TLA+. And he just gave an example. Like he said, I had an intern who was great, but that intern went off and got a job. And when that intern got that job, he was told at work, stop doing TLA+. It's a bunch of extra work. Don't do that anymore. And my part was like, you have to stop and think about what you're writing. You can't just hack it out. And I wrote down the next thing he said. This is a quote. He said, thinking is a very hard sell. Most people would rather fight than think.
Mike
Yeah, it's probably going to be even a harder sell as time goes by. And we have tools to do it for us. Yeah, the title of his initial talk was Coding Isn't Programming. And from my perspective, he was kind of preaching to the choir. So there was not a lot that I found in his thesis to disagree with. Maybe a slight misalignment on the idea that you shouldn't care about programming languages because I think programming languages are cool and I think some of them are better than others.
Erik
Yeah, yeah. There
Mike
were a couple of ideas that he talked about which I really liked or that resonated with me, I guess. One quote that I wrote down was, to think rationally, you have to know simple logic. So I thought that was something that you don't really think about a lot as a professional programmer. I've been reading the Hillel Wayne's logic book recently, and it's surprising how much stuff in there that you use all the time, but you don't really think about using. So I like that idea. He also had this He was going through this example, which ironically had an error in it. Oh, in the talk, yeah. Yeah, he was talking about, you know, the state transitions, and he actually had an error in his slides where he had the wrong value for a particular state. But anyway, he talked a little bit about how you would validate that a program was correct, and the proof step is something that most programmers couldn't do. And he also had this line about how the people who can't do that stuff are probably going to be the first people replaced by the AIs.
Erik
Oh, yeah. Shots fired there, huh?
Mike
Yeah. I'm not entirely sure that I agree with that, but it is an interesting thing to contemplate. It's hard to disagree with the idea that this whole vibe coding thing is a lot more along the lines of what we typically do as coders than the sort of thinking and abstracting that he was talking about.
Erik
We just dribble out lines of programming language or puke them out or some other verb them out. I want to go back to your comment about programming languages because I had the exact same hangup. I'm like, but I like programming languages, Leslie Lamport. So at the end of the talk, I really wanted to ask him a question. It just bubbled up, and it was based on his writing. I just was like, I got to ask him this question. So I waited in line for like 30 minutes, huge line, and I honestly felt kind of bad. He looked fatigued. He's 84 years old. So in this book, A Science of Concurrent Programming, again, this is a PDF you can read for free on his website. It's not published in print form. He says something like, fancy types in programming languages, they allow you to express a type like a non-negative integer, which can prevent you from compiling a program where you're dividing by zero. But it's a lot of effort to create and work with fancy types. You don't even really need these. You could just use assertions instead. This is his justification for why TLA plus is untyped and how you can still validate abstract programs with it. So this line about, and it's just a throwaway line. It doesn't go on and on and talk about typing. This line about fancy types has been stuck in my brain since I read it. So when I got a chance to ask a question, I said, Professor Lamport, thanks for the talk. You said programmers are hung up on languages. They are always thinking about programming languages. I'm a programmer, so I'm hung up on programming language, so I have a dumb question for you. And he had this look at his face like, all right, what is it? So I repeated his argument about fancy types back to him. And then I asked him, if you had to do it over again, if you're going to write TLA Plus today, would you reconsider using fancy types? And he looked at me. He was like, the cock people, now Ruck, they argued with me so much about this years ago. People fought me so hard on this, he said. And then he kind of thought about it for a second and he said, I wouldn't do it any differently. He didn't respond impulsively. He put his hand up to his head and he thought about every question people ask him. But then he said this thing that's been kind of bouncing around my brain ever since, the rest of this week. He said, the math that programmers use is so basic that you don't need fancy types to express it. And I was like, thanks, Professor Lamport. I gave him a sticker for the show. And I said, hey, we talked about your work on our show. I just want to say thanks for all, thanks for everything. And then I walked away. Just sort of like the math programmers use is so basic. What the hell does that mean?
Mike
Yeah, there are various interpretations of that, I think. I guess my take was he just means that it's simple logic and simple logic is not super hard, but he could also mean basic in the sense of fundamental.
Erik
Yeah, I went back to his book, A Science of Concurrent Programming, and there's a line in there. Chapter three is about, I can't remember what it's called, but it's like foundations of math or something. And he's like, I'm going to teach you some math in this book. And it's basic math, no harder than arithmetic. and he writes in there again we're talking about abstract programs right mathematically he writes the behavior of a digital system or abstract program is an infinite cardinal sequence of states where each state is an assignment of values sets to variables and i read this sentence and i'm like oh, okay, I think I get it, but is this a sentence of math? Is this mathematical?
Mike
There's a difficulty where people tend to think of math as being equations and symbols, and so if things are described too informally or just in words, it doesn't seem quite like math. But I think it's
Speaker 3
probably
Mike
more true of mathematical logic and discrete math but it does get described by words more frequently.
Erik
So that talk was interesting, and it's something I'm going to remember for a long time. Did you know that Lamport originally conceived of TLA Plus as a language for doing proofs only? He didn't actually think it was possible to build a model checker, and there was a colleague who wanted to work on that, and he said, no, it's not possible. But I think he was probably happy to be proved wrong when the model checker was produced. That tool is called TLC. It's written in Java. You can download it. It's open source. And you can run checks of written TLA Plus specs with it. I did not
Mike
know that.
Erik
I think I'm going to think about my meeting with Lamport for a long time. I should have gotten a photo with him. I guess I'm in the photo with Rob and the other folks. Rob was like, hey, let's get a big photo with Leslie Lamport. I'm in that photo. You and I should have gotten a photo with him. A lot of people were up there like, let's take a photo, Leslie Lamport.
Mike
I took a photo of you with talking to Lamport. It's me in the back of his head.
Erik
Yeah, he's sort
Mike
of turned to the side, so you can't see his face. So it could potentially be a Leslie Lamport impersonator, but
Erik
it's not.
Mike
It's not to trust us.
Erik
I just was not focused on the photo. I was focused on this dumb question that I had that was burning in my brain. And I got it out and then ended up with new questions. Isn't that always the way, Mike? My soul making connections in the measureless oceans of space, trying to build bridges to stuff, Trying to understand.
Mike
Yeah, and me standing around trying to convey to people that I want them to leave me alone. I thought this was a pretty inspiring talk for a couple of reasons, I guess. One is that it's kind of in a contrary direction to the current state of the programming world, which is kind of like we're all going to be replaced by robots.
Speaker 3
I
Mike
like that about it. And then the other thing that is kind of inspiring to me about this maybe would not be as inspiring to somebody who were younger is that it really, I really like the fact that he's 84 years old and he's still out there, you know, giving talks and advocating for things and seems passionate about this stuff. He's only a few years younger than my father. And, you know, my dad is a great dude, but he's, he's definitely not, uh, he's not
Speaker 3
out there.
Mike
He's not out there giving talks about his profession anymore. So the idea that, you know, 20 years from now, I could still be out there striving is kind of inspiring.
Erik
Still sharp.
Mike
Yeah. Yeah. I mean, he clearly is still able to, you know, think on his feet pretty well. And this was a pretty polished talk.
Erik
All the slides written in La Tech.
Mike
I do, like you, I think have sort of a disagreement about the programming language thing.
Erik
And at the moment we're
Mike
recording this, there's this sort of controversy that's been in the news about Microsoft implementing TypeScript in Go.
Speaker 3
So Microsoft
Mike
wrote this TypeScript in Go and everybody's saying, why didn't you write it in Rust? And, you know, there's been some fairly well-reasoned articles on why they chose Go over Rust and, you know, what the obstacles were with Rust. And so my point being that I think programming languages do matter, you know, even when you're not that you don't have to think and abstract, but also the coding does matter.
Erik
Okay. So how do you reflect back on scale? I've been thinking about it all week. For one, I'd like to go back next year. That was a rad conference. And when I go back, seeing all these volunteers working so hard as a volunteer-run conference, it makes me wonder, do they need any help? I'm up for helping them.
Mike
Yeah. Yeah, it would be fun to be kind of behind the scenes. I don't think I have networking skills that would
Erik
help
Mike
out Rob's team very much.
Erik
Or NICS. They're using NICS to spontaneously spin up all their stuff.
Mike
Yeah. Yeah, I would like to go back, and I would definitely consider presenting if that were an option.
Erik
What would you, if you're going to give a talk on something at a conference, what would it be about, Mike?
Mike
I think if I were going to give a talk at a conference like this, that's, you know, fairly broad. I think as of today, the thing I would probably be interested in talking about is the local first software movement or maybe something specific about that. This is something I've been thinking about a lot recently and that kind of intrigues me. And I think there's maybe a slight touch of nostalgia to it as well since I started out in the world where local first software was – there wasn't really – it's kind of a retronym in the sense that when we were back in the 80s, everything was local. So we didn't really think of doing stuff in the cloud at all. But it intrigues me both from a software engineering standpoint and also from kind of a political and philosophical standpoint. I find the AIs fascinating, but I worry a lot that they are kind of in the hands of companies that are hard to compete with. And it may turn out that we can eventually run these things locally and maybe there will be a technological development that allows us to train them locally and computers get more and more sophisticated. But as things stand with the huge amount of hardware that you need to train them and the huge amount of money it costs to train them, it feels like things are becoming more and more concentrated in a handful of cloud companies.
Erik
Yeah, and that's kind of scary. It's like having a gym membership for using your tools and your workbench. You go in, you pay your monthly fee, and you get to build stuff on site in their building with the tools that are there. And then when you leave, you don't get to build anything anymore. That's kind of sad to imagine.
Mike
Yeah, and especially in the environment we're in where, you know, data sets that we think of as being public are being pulled out of the public realm and organizations that are producing data that is potentially politically controversial are being defunded. And the idea of having data be available in a less centralized way is kind of intriguing too.
Erik
That kind of spirit was present at scale. I did like scale. I like the idealism. There is something inspiring to me in there. It makes me want to go to conferences where people are like, hey, I built this cool thing. Isn't that fun? I want to go to those conferences and talk to those people who are enjoying making things. That sounds like a good time.
Mike
Yeah, same. I used to go to the PyData conferences fairly often and presented a couple of times. And conferences are the most fun when there are people there who are doing things that are similar to what you were doing, but also advanced in some direction or a lateral move in some way so that you can sit down and say, hey, you know, what can I learn from you? What can you learn from me? And that kind of thing. So
Erik
I
Mike
look forward to being able to do more of that in the future.
Erik
Me too. All right. Let's try to get to scale next year. It was a lot of fun. Go to the conference. And I think we'll be back next week with some regular content. so friends if you'd like to support the show see us on patreon patreon.com picture me coding if you'd like to reach out you can send us an email podcast at picture me coding.com and you can also reach us on blue sky under picture me coding this has been picture me coding with eric anchor and mike mull thanks so much see you next time bye-bye