episode64_57143b322f

[!note] Machine transcript Transcribed locally with whisper. Names, jargon, and code identifiers are often wrong — check any quote against the video before putting it on a wiki page.

Transcript

[00:00] (upbeat music) - Baye, windows, one more episode of the Type 3 referral podcast. As always, this is your host, Pedro Briel. And in today's episode, I have the great honor to have with me, Sriram Krishnamurthy. Sriram has devoted his entire career to advance the teaching of programming and programming languages. He's a professor at Brown, the author/co-author of different books about this, and a major contributor of their record programming language. In this episode, we talked in depth about why PL education is so important. What can students really gain from it in practice? What changes in the age of AI? Is programming even going to be a thing in the next years to come?

[01:04] I'll keep this intro short because this is a lengthy episode. We definitely had a lot of interesting ground to cover with Sriram, but if you're new in this podcast, please subscribe, click the like button and all that. A huge shout out to our patrons. You really make this show possible. If you enjoy the show because they're becoming a patron with as little as $5 a month, you'll get your name in the screen like this and access to exclusive Discord channels depending on the size of the donation you also get to exclusive behind the scenes content released together with each episode. Simply go to our website, type3referall.com/patreon and become part of our awesome community today. Now, without further ado, let's get into this episode. (upbeat music) Hello, everyone. One more episode of the "Type 3 Referall" podcast. As always, this is your host Peter Avril. And today with me, I have my amazing co-host, Dan Tukin. How are you doing, brother? - Happy to be here as always. It's really a pleasure.

[02:06] - Oh, that was so enthusiastic, man. I could feel you're so being drained out of you. What has industry done to your soul, man? - I think I've given the same kind of responses I always do. I think of myself as like a fly that gets into the room before you have a chance to close the door and it would be too much effort for Pedro to shoo me out. So he just keeps hanging out. (laughing) - That's not true. I'm always on his ass being like, "Hey, Dan, let's do something. Let's record something. Hey, Dan, hey, Dan." (laughing) Anyways, I am very happy with our guest here today. Actually, I usually ask, I did a terrible job. This was, I was forgetting. I usually ask how to actually pronounce your name and I forgot about that. So please pronounce your name for us and let me know if I got it right. - Sri, Krishna Murthy? - Sri Ram. Yeah, sure, whatever. Sri Ram is fine. Sri is fine. Anything's fine. Hey, you is works too, in the right context. - I usually start by asking the person, the guest, to introduce a little bit about himself.

[03:10] Like what got you into programming languages? How did you get to be where you are and things like that? So we and our audience gets to know you a little bit more. - Okay. So, hey, thanks for having me on. This is an amazing podcast. You folks have really done your research. I'm excited to be here. So my name is Sri Ram. I grew up in a city called Bangalore in South India. I was one of those people who stumbled into programming. I was sort of, I was excited about physics. I was really excited about physics of the very small, like subatomic physics. And I was really excited about physics of the very large, like astrophysics. And I thought I would end up becoming a physicist. I mean, in retrospect, I would have been like a third grade or third rate or fourth rate physicist. And then computing came along and saved me. So I could be, I don't know, maybe a second rate computer scientist instead of a fourth rate physicist or something. So I was excited about physics and then I discovered programming and it was super exciting. I think I know the moment when my life and programming languages really became a thing for me.

[04:14] Now you don't understand like, you know, this was India in the eighties and I don't know if things have improved massively, but the educational system was a lot of like rote learning, a lot of memorizing, you know, a lot of words over ideas. Right? And so, you know, so I knew the names of lots of programming languages, even though I'd only programmed in one. I could tell you all kinds of facts, supposed facts about these languages. COBOL, everyone knew, was the business oriented language. So you used it for business applications and FORTRAN if you wanted to do scientific computing. I had never seen a COBOL or FORTRAN program in my life. There were no artifacts that I could see. I just knew the names of these things. And so one of the other languages I'd heard about was Pascal. And there were very few of us in Bangalore at the time who knew any computing. So we would sort of talk to each other. And one of my closest friends, Rustam Guzder, Rusty, who's now a doctor, Rusty basically, Rusty and I would like code together. We were like, we had like amazing experiences coding and, you know, working together on various things. And one day I remember the street we were walking down in Bangalore and he said to me, so his brother had gone off to college.

[05:20] And in that college, they were teaching his brother Pascal. Now I had heard of Pascal. I was aware of the existence of this language called Pascal. I knew it was created by a guy named Niklas Wirt. Never in my life imagined somebody had meet Niklas Wirt. But, you know, I was aware of the existence of these people, but I didn't know anything about Pascal. So anyway, we're walking along the street and he says, so here's the thing. Now you have to understand, the only thing I'd ever programmed in was BASIC. That's the only language I actually knew, right? That I, as opposed to knew the name of. And Rusty says to me, he says, you know, the thing about Pascal is they don't have any go-to statements. And I remember stopping him in the middle of the street and staring him in the eye and saying like, how on earth can you write a program without go-to statements? Like how can you write a non-trivial program without go-to statements? And that was a mind expanding moment for me that there was a way of programming that you could actually write a thing and you could take away the one thing that I felt was essential to being able to write programs.

[06:24] I think in retrospect, that was like a really profound moment for me. You know, I had summer to myself, not much going on. So I remember thinking like, it'd be fun to write a program that could read another program. So I ended up writing maybe the world's worst ever meta-circular interpreter because I was in BASIC, right? Like I didn't know the concepts nobody, I didn't know anybody around me who knew meta-circular interpreters. One of the key features of my language is it had only 26 letters, 26 variables, because I had an array for, you know, size one through 26. So I could look up the variable name and the array to get its value. But you know, so I did lots of dumb things like that, but I think all those like dumb things were like super formative, like all these weird kinds of failures are super formative because when I eventually got to places and people who knew things, I think I was prepared for like actually understanding them. I was like, "Oh, that's the thing I was trying to do really, really badly once upon a time." You know, things like that. So that was my experience. - It seems like programmers generally are excited about like things that you can do in a programming language and programming language people get excited about when you can't do something in a programming language.

[07:32] - Yeah, yeah, yeah. It's this amazing tension between like enabling things and preventing things and like, you know, like later in life, I studied a whole bunch of computer-aided verification and you know, one of the things you, one of the early things you learn about writing properties is you learn about the decision and liveness and safety, right? And roughly speaking, safety is prevent bad things from happening and liveness is eventually good things should happen, right? And I viewed that as like a recipe for life, right? In general, in life and certainly my research program, I've tended to always have like two projects going on, one of which is like preventing bad things from happening and the other is eventually make a good thing happen. So I think, you know, that's the dual, that duality, that tension is central to how we think about the world. Yeah. - And learning, Lane, you said you were learning Fortran. Is that right? That's the language you were writing? - Well, eventually I found, eventually I learned some Fortran and COBOL. Yeah, eventually I got access to those. Yeah, yeah. - Was that when you decided to go to CS education? - I think once I started programming, I was pretty clear that I wanted to do computer science. That was pretty obvious to me.

[08:34] Yeah, it was just like, I felt it in my bones. My idea of summer fun was I would sit there and like, sketch out data structures because I didn't know that was a thing and I'd be like, how would I represent this thing? So I was that kind of nerd, you know? So, I mean, again, probably invented terrible data structures, but, you know, it was, I considered it fun to try to design a data structure. So I think I was just hooked early. - Weren't you also a literature student? - Yeah, so that was the thing that got me out of India. I really wanted to study humanities as well. And you can't do that in India. Like you, I mean, now you can, but back then you either went to an engineering school or you went to like a arts program or you went to like a literature program or something. And, you know, you couldn't take both of those, like, and even there the curricula were very prescribed. And I, some through a long uninteresting story, I got hold of like an American college catalog and somebody gave it to me and I looked at it and said, wait, you can combine these and you can do whatever you want. And like, yeah, and I'm like, okay. I have to figure out how to get there.

[09:36] So you have to like, you know, take some exams and score high and you can get a scholarship. So I took some exams and got high scores and got enough of a scholarship to come to the US. And so that's how I got to do, you know, humanities and computer science at the same time. Yeah, totally. - Why didn't you pick the humanities? That's like so much better, obviously. - Oh, it's so much fun. I mean, I think, you know, I wrote to my best friend, I was actually thinking about grad school. I was also very excited about, I was studying philosophy and philosophy of science and that seemed like right in the middle between everything else. And my best friend basically wrote back and said, you know, these are great topics. You might wanna consider that maybe the job prospects in computer science are better and these are things that you could maybe do in your spare time. And I said, that's a interesting argument. And so I put away the graduate school applications in philosophy of science and stuck to the grad school in computer science. So completely purely mercenary reasons in other words. Yeah, sorry, Dan.

[10:40] - But you still made it hard for yourself. You had to find a way to make it hard for yourself by being a programming language person. So like you always put in, you know, the weights. - But I think that in some sense, I think like a lot of PL people have some attachment to language, right? Like I think that literary thing is, you know, like there's something about language. And so there's some people who don't care about natural language. And then I think, but I think part of the reason the PL community in general has very high standards for writing and people tend to write well, is I think a lot of people in PL just inherently like language, whether it's natural language or programming language. And that leads to like, you know, just like we wanna find exactly the right construct, we also wanna find exactly the right word. We wanna write, you know, we wanna, some people wanna be more spartan, you know, Dan and I have discussed this on certain social media. Some people wanna, you know, some people write like Faulkner and other people write like Hemingway. But the point is those are styles and we can identify styles. And I think we are more in the realm of knowing about styles and understanding styles. And it's not surprising that there's carryover between, you know, natural language and programming language at some level.

[11:45] I won't read too much into it, but I think there's certainly something there. I think there's a lot of us who feel like some affiliation with thinking about language more broadly. - So remind us where you went to grad school. How was the process there? Finding an advisor and your topic? - Oh, that was funny. Yeah, so I went to Rice and I went to Rice because I was very excited about algorithmics. I thought I wanted to study algorithms. But I also had in the back of my head, I was kind of excited about I had been exposed through a very weird set of circumstances to Dan Friedman. I didn't study at his university or anything else. But my best friend went to grad school at Indiana and then he introduced me to the person who's now my wife who was also a grad student at Indiana. And so they were friends and that's how I got to know my wife. Basically through Dan Friedman's course, more or less. And so essentially what happened is they were sending me homework problems. Like my friend was like, look, you're a little bored. I'm just gonna send you the problems that I'm working on in Dan's course. And I started working on the problems.

[12:46] I didn't know, I wasn't sure if the solution's right. I was like, what do I do? They're like, well, just email Dan. I'm like, what do you mean just email Dan? Like, well, that's what we all do. When we think we have a solution, we email it to Dan. I'm like, oh. So I just started emailing him and I was like, at some point he's gonna ask me like, who the heck are you? You're not studying, I just don't even live in my state. And I was like, if he doesn't ask, I don't need to tell him. And then about 10 weeks in, he's like, who are you by the way? So I was excited about PL as a thing, but I was also really serious about studying algorithms. And I had these ideas. I wanted to study numeric algorithms because I was really annoyed by floating point numbers. I studied floating points, I was like, this is terrible. And then I found like papers, PL papers that said, oh, we could use, I was like obsessed with continued fractions. I somehow got into conversations with Bill Gosper. And so I was really obsessed with continued fractions. And then I found there were PL papers that said, you know, continued fractions are like, you know, infinitely long data structures, but PL has really great ways of representing them using closures. I'm like, oh my God, like everything's coming together. How amazing is the world?

[13:48] So I had this in the back of my mind. So I picked Rice because it had a really great PL group, but I was also gonna study algorithms. And I did that. I ended up doing CompBio for about a year and a half. And then I read this one paper by Mathias Felison on the expressive power programming languages. And it just blew my mind away. It was just like, what a beautiful, what a stunningly great piece of work. And I was also like feeling nervous about being in CompBio because I had never been a great bio student. Like I think now, I think would be a great time for me to start studying biology. And I have been studying some biology because it's such a beautiful field. And it's like this, and I think for people who care and love thinking about systems, it's a fabulous field for people who care about systems. But that's never, that's certainly not how I was taught it. I was taught it as like taxonomy, like the old Ernest Rutherford jibe about everything other than physics and stamp collecting. It's like there's 27 kinds of these and four kinds of that. And there's trees of this and trees of that. And like, what are we doing here?

[14:51] There was no structure. There was no semantics to any of it that I could see. And then it turned out, everything has semantics in biology and it's not just genetics, everything has semantics, but nobody ever explained it to me in those terms, the way like physics had been explained to me. So I was feeling really nervous. I'm like, I don't think I'm very good at biology. I don't know any biology. And sooner or later, I don't think I can keep faking it in CompBio. Somebody is gonna find out I don't know any biology. Like my math and computing is gonna get me only so far. I think I need to bail out. And so my bailout was like, I was trying to think, I was like, what should I do? And then I read this paper and I was like, that's what I should do. And sort of dumb luck, the person who wrote and written the paper was in the same department. So I went over to Matthias and tried to convince him to take me on as a PhD student. And that's how I ended up in PL. - So could you recap like briefly what that paper is about? - Yeah, so what does this paper say? Yeah, so, you know, I gave a talk about it in Papers We Love. So if somebody is interested, I would say go, I mean, you should read the paper.

[15:53] That's what you should really do. - You should watch the talk first and then you read the paper. It's gonna be so much easier. It's a great talk. Thank you for doing that. - I'm not gonna say that, but if you feel that's great, that's wonderful. That was my hope. So the thing about the paper is it asks the following very fundamental question, right? We have lots of languages, we have lots of language constructs and we spend all of our time arguing about like, language X is more powerful than Y or feature X is more powerful than Y. And how can we put that on any, like, and it's all a matter of opinion, right? Like if I asked you, you know, are generators more powerful than async? And be like, I don't know, I think so. And then somebody else would go, I think I'm not sure, I don't agree, right? And it's all a matter of opinion and it feels like we can't get past opinion. And the only mathematical framework we have is Turing completeness, but all these things are Turing complete, right? And so it's, you know, to use Alan Perles' phrase, it's like the Turing tarpet, right? Once you enter the tarpet, you can't get it back out. So there's no meaning, like, yes, Chomsky hierarchy stuff like that is great.

[16:57] We can talk about regular context or context. But the moment you get to Turing complete, it's all game over, right? And then of course people say like, look, all these debates are meaningless because they're all Turing complete. So it doesn't even make sense to talk about is one more powerful than the other, right? And that is kind of, that was the state of the world. And what this paper says is, somehow I don't think that's quite right because when we say X is more powerful than Y, we have some intuitions about what we mean. And the astounding thing this paper does is it says, let's take that human intuition and let's try to categorize what it might be saying mathematically. And what it offers as a framework is the idea of macro expressibility, right? So if X is locally transformable into Y, then X does not, like basically you can just, you know, if you could write a macro basically to turn every X into a Y, then X is really not adding expressive power, right? So the more interesting cases, you know, so for example, if you have like a for loop, you can turn that into a while loop through a local transformation. So given while in a language, for doesn't really, yeah, it's convenience, but it doesn't really add expressive power because we can do this macro transformation.

[18:06] So then the interesting question becomes, that's the easy part, right? The interesting question becomes for something to be expressive, it must be impossible to do that transformation. It's not just, I couldn't think of it, but there is no way to do that as a local transformation. And that's what the paper sets up. It sets up this machinery for us to be able to, you know, it uses program equivalence and sets up this machinery by which it is able to demonstrate, for example, it shows that if you have a language without state and you add mutation, mutation is expressive. And if you have a language with like state mutation, but not continuations, continuations are expressive. So it's that the real power is being able to say, I will demonstrate to you that it is impossible for there to be a local macro for this. It's like, that was mind blowing. So first of all, it asks the question, right? That was already the amazing thing about it. There's a question, and instead of all of us just saying, it's just a matter of opinion, what can we do, Turing completeness, game over? It says, why don't we first try to think hard about what we might be trying to say when we say this? Then it says, I'm gonna pick a particular definition and you can dispute the definition, some people do, but it's still a reasonable definition.

[19:16] It's at least a reasonable definition. And it sort of inspires you to maybe come up with your own definition, right? Once somebody puts a stake in the ground, you can then come up with your variation of it. Then it says, okay, so now we've got this machinery, we're gonna work through some interior, it doesn't work through the examples, that's kind of what I do in the talk. But when you work through the examples, you're like, yeah, yeah, yeah, yeah, I kind of believe this so far. And then the hammer blow, right? Like, we're gonna show you the things that are expressive. And those also somehow correspond to the intuition we have. Like if you have a language without state and you add state to it, it feels like we've really added something of substance to the language. And it says, here's how we're gonna demonstrate that. Like, you read that, you're like, oh my Lord, what is this? This is like, how can you, I didn't know we could do such things, you know? Like, I feel like maybe it must have felt that way when somebody first came out of the Chomsky hierarchy, right, people must have been like, I mean, of course we didn't quite have computers on top, but there must have been the sense of like, we've just discovered some deep structure to the universe that we didn't know was there before. And this paper felt the same way to me. And it was like, there's deep structure and we've found a way to like pin it down mathematically, no opinion, math, right?

[20:21] And that was transformative, yeah. That's why I built the talk around that because I want everybody else to get that same sense of like inspiration, so. - The thing that kind of surprised me about that paper was that like, I don't really see it referenced it. Like, it seems like such an earth shattering thing. - It's like a cult paper. And in fact, that's kind of actually, I had a choice of two or three papers I was thinking of for that paper as we love to talk. And I picked this one because it is the least cited of the papers that I had in mind, yeah. And so I was like, let's pick the most obscure one. - I actually bumped into that, like surprisingly, I actually bumped into that paper during my research because I was trying to understand what's going on with JDTs, generalized algebraic data types. And I was like, wait a second, this feels more expressive than regular algebraic data types. Like, is it really? Can I show it and I started trying to figure out what does it actually mean? And then eventually I stumbled upon this paper and I'm like, why, nobody else is talking about this. This paper is from the seventies and it's, that's it. There's nothing else after that.

[21:24] Like we stop this upstairs. And then I started trying to come up with that formalism and I couldn't actually, it was a little over my head, but the year later, the year that I graduate, someone actually proves that and it's a beautiful Popo24 paper showing that generalized algebraic data types are more expressive than regular data types and through micro-expressibility of the license. And I was like, wow, this is the paper I wish I had written, you know, this is awesome. - Yeah, I don't know. It's a little obscure, but yeah, so what? There's lots of beautiful papers that obscure lots of not so beautiful papers that aren't, it's fine. It's the nature of papers, yeah. So talking about beauty and about design and about languages and about what things mean to one another. How do you perceive the notion of beauty on languages or on teaching languages? Like what is, what's your philosophy here? - You know, one of the things that we have a lot of difficulty coming to terms with is that ultimately programming languages are things that humans have, like have emotional feelings about.

[22:40] And it's, you know, I'm on a type theory podcast, type theory for all, and it's like nothing could be further from that, right? But I think we run into this problem because we don't wanna acknowledge it, right? When people try to convince somebody else to pick a language, it's always like, I'm gonna make the strongest technical argument I can. It's like a math argument, performance argument, whatnot. But we don't wanna really come to terms with the fact that people also have like emotional attachments and disattachment and dislikes for things. And you can't overcome that, right? I mean, I have said in public before, I'm completely comfortable and happy to say, my favorite syntax is raw, parenthetical. I love parenthetical syntax. The first time I saw it, I'm like, okay, this is it, game over. I don't know why anybody invents any other syntax, right? But I also, you know, it's funny, I describe parenthetical syntax, it's like, I'm also left-handed and I feel like it's the same thing, like we're not enough of a population to actually get, like, you know, you have to go to a store if you wanna buy like a left-handed scissors, right?

[23:44] Like everything in the world is not, most things in the world are not designed for us, right? But we're also not small enough of population to just like disappear, right? I don't know, we're like some weird, evolutionally stable percentage of like, I don't know, 10 or 15% or something like that. And we just keep like shuffling along generation to generation, right? We don't just die away either, right? And I think parenthetical syntax is the same way, there's like 10% of the population or something like that, like, oh my goodness, this is so beautiful. The other 90%, like what is wrong with you helping even? And then like, no, no, no, we don't see the parentheses. Like, what do you mean you don't see the parentheses? They're right there, right? So the thing is, and you know, I've said this to people, they're like, well, you know, I think I could convince somebody something something like, look, it's like ultimately, we have emotional reactions things. They're like, no, no, no, I don't think that's entirely true. I'm like, okay, how about I take everything you said, and I'm gonna give you the same language you're describing, except it's gonna have a parenthetical syntax. They're like, oh, yeah, maybe I'm not. Yeah, okay, yeah, right, right? So, and in fact, you know, when we built pirate, 95% of the reason for building pirate was just to like not do parenthetical syntax, right?

[24:54] We had pedagogic ideas that we thought were really important. And it was obvious to me that the syntax was our biggest blocker because every time you drive a conversation with somebody, they'd be like, well, you know, but what about the syntax? Like, no, no, no, don't worry about syntax, but you can't tell somebody don't worry about the syntax. Of course, like the moment they brought it up that obviously it's the only thing, you know, and we also know this thing from education that like learners always focus on the most superficial aspect, right? And I mean, superficial, I'm using superficial in two ways, by the way. Superficial is, you know, it's kind of a pejorative, oh, they're superficial, but I'm actually, by superficial, I mean, on the surface, the thing that is most evident, the thing that's most visible, right? So a learner is not looking at the lambda calculus underneath. They're looking at the parentheses because that's all they can see right now. They can't see past that till they've learned the thing, right, or they're seeing the indentation, they're seeing the syntax before they can get to the semantics. That is just what it means to be a learner. There's nothing wrong with that, right? And so we'd go to educators and they were also learning and they'd also be like, oh, the syntax.

[25:57] And so, you know, we built Pirate basically to just say, like, okay, let's get that off the table, right? Let's see if we can have this conversation without that. And I think we've had much more, we've had a fair bit of success with Pirate because that is no longer a topic on the table, right? So I think it's, I think, you know, notions of beauty and so on are interesting. I think they're definitely fairly personal. You know, I've been very, I have done semantics work. I've been very comfortable talking to people who would describe themselves as object-oriented people. I think at heart, I'm mostly like a functional programmer. But I've worked enough with object-oriented people and done research on object-oriented languages and so on that it's clear that for them, that is a native way of thinking about the world just as thinking about mostly functional code is my native way of thinking about the world. And everybody looks at these other things and we can look at them with respect. We'll be like, well, you know, it's like my, how can you program without go-tos, right? Same way, like, how can you program without giving me side effects?

[27:01] Like, what does that even mean, right? And same way, the objects folks look at it as like, how can you program without even having objects? And then if you're like an Erlang programmer, you're like, how can you program without having like amazing lightweight concurrency? So Paul Graham has this great, what he calls a Blub Paradox, right? So the Blub Paradox is, and he very carefully says, there's a language, you have a language called Blub, right? And Blub is, it's like, it's just about right, right? And you look at all the stuff that's not in Blub and you look at people using languages with stuff that's not in Blub like, how can anyone possibly program without those things? And you look at all these languages that are bigger than Blub and you're like, who needs any of those things? Like, I've programmed in Blub for decades without needing any of those things, right? And we've all got our blubs. And I think the moment you realize that and you recognize that each of us has our own blubs, this is not to say there are not like mathematical properties, performance properties, and all these other things. Of course there are, right? And, you know, but I know I'm preaching to the choir when I say those things. I think we just as a community have had a harder time recognizing the sort of the emotional human side of that, of PLs.

[28:07] - Right, I think it's very interesting how you bring up the factor of waiting in how people think and learn about languages when designing the language. What else, how would you describe your process or the process that you've learned that works best in terms of designing a language? What is the hierarchy of things that you should have in your mind? And which obviously, as you've mentioned, includes how people think about the languages. - Yeah, so I, there's a thing I sometimes like to say that like every language is actually a domain specific language, right? We went through this period when we thought like there were things called general purpose programming languages. Again, you know, like if you look in the right, if you look at a 1980s PL book, they'll tell you like, you know, we had domain specific languages, but we have general purpose languages, right? But I find it amusing that if you go back to the, and you're like, okay, what are the oldest general purpose languages? They're like, oh, you know, like COBOL and Fortran. Well, COBOL's name is Common Business Oriented Language. Fortran's name is Formula Translator. Algol's name is Algorithmic Language.

[29:11] LISPs is List Processing, right? They were domain specific languages that somehow got morphed into so-called general purpose languages. But, you know, you take your so-called general purpose language and you try to do a thing that it's not particularly designed for, like, you know, massive concurrency or massive distribution or massive whatever, and it completely falls down. So how general purpose can it possibly be, right? It's just that we've just defined a sort of like happy medium of like, I don't know, Webby server desktop applications that don't need to scale very much. And then we call that general purpose, right? So the thing is like, I think we always design around domains, whether we like it or not, whether we acknowledge it or not, right? And if you take that point of view, I like to think that the best way to think about language design is, and this is certainly the thing that inspired the way we thought about like, you know, Flapjacks and Father Time and things like that, is you want to think about the needs of the domain, like the domain is providing the pressure on you. I've also, you know, built like network programming languages, things like that, where the domain comes with its own constraints, right? And it's providing a whole bunch of like backward pressure on your design that you have to accommodate.

[30:15] And then the challenge is finding the right computational medium that then lets you most naturally put together the things in that domain, right? That's, I think, like the subtle thing that leads to generally comfortable designs is you let the domain express itself, and then you figure out what is the right computational fabric for weaving together things in this domain. And that's not necessarily the right one, I should say, that's like many, but like find one that's like happily compatible with this, that, you know, is somehow going to lead to like, you know, maybe the best expressiveness or the best performance or the least errors or whatever. So I think that is one way to think about language design. These days, when I do things in a pedagogic context, I think I've got another perspective, which is, it's not mutually exclusive, but having done a lot of research over the years into misconceptions that people have, I think a good way to think about language design is try to figure out how to avoid the misconceptions in the first place, or how to surface the misconceptions, and everything from the programming language design to the IDE design to various other things, error message design and so on, can all join in either creating misconceptions or reducing them or eliminating them, and that becomes a really useful principle for language design.

[31:30] That's pretty abstract, I know, but, you know, there are two different principles. - It makes me think about how, in undergrad, I had an algorithms professor who he was obsessed with this idea of conceptually simple algorithms, like how much can we do with a very simple algorithm, and it ended up becoming very approximation algorithm-heavy. And I came up to him, I was already interested in programming languages at the time, and I said, oh, how does this relate to programming language theory? And he said, well, I'm more interested in what you say rather than how you say it. And at the time, I didn't have a response to him, but I felt kind of intuitively like this should really be connected because the kind of language that you have will shape the kinds of things that become conceptually simple. - Every PL person is at least a mild, superior Warfian. Otherwise, you wouldn't exist in this field. - The superior Warfian language-- - Yeah, yeah, the belief that our language shapes our thought, right? It's a controversial thing in linguistics, but I think it's, you wouldn't be in the field of PL if you didn't at least subscribe to the mild version of that theory.

[32:34] - Yeah, so what exactly, I don't know. I don't actually have a question that's connected to this. It just seems kind of interesting that there's this shape to problems, that there's these two different aspects of it. There's the people who do things who I feel kind of mildly inferior towards, and then us who try to bring the language to those people to make those things simpler. And the relationship between those has always puzzled me. I mean, look, I, as somebody who's read a lot of algorithms books, I think part of the problem is the, there's a sort of unstated programming language in algorithms books, and it's this sort of like this. So we've been using this term that we call small, which is the standard model of languages. So small is my name for, my PhD student, Feng Chen and I have been using this term, is our name for the semantic core that is common to everything from Java and C sharp to like Python and JavaScript, to like Racket and OCaml, right?

[33:43] Not Haskell, not Prolog, right? But basically languages that have first-class functions, first-order variable names, first-class values, mutation, garbage collection, a collection of principles like that, right? So even whether you have objects or not, whether you have like, you know, classes or not, underneath like semantically, they all have the shared, they have this sort of similar structure, right? And this is kind of the language of algorithms books with sort of a mutation-heavy feel, right? And I think it has, so in some sense they don't, when people say, "I don't care how it's expressed," like you actually kind of do. If I told you to write that same algorithm in Prolog, you would actually care deeply about how it's expressed, right? What I mean by, "I don't care how it's expressed," is I've got this like medium that we have not, we've never really sat down and voted on, but we've just decided on, right? It's not quite the Turing machine either, right? Like this, it's, yeah, it's not the Lambda calculus, but it's not a Turing machine either. But we've just kind of agreed upon this. It's not even, in fact, most algorithms books are like first-order, right?

[34:46] There's maybe a little higher-orderness, like, oh, maybe sort will take up argument to like decide which way to sort. But they're all like, most of the algorithms you read, you know, you go through most of these textbooks, they're all like first-order functions, right? And there's barely any higher-orderness there, right? And that common medium is like kind of what we've accepted, I guess we've been forced to accept as our medium, right? And I think that that's kind of unfortunate, actually. So, you know, one of my favorite examples of this is when you try to teach, you know, dynamic programming, right? I think teaching dynamic programming first is actually a pretty bad idea because it obscures what's really going on, right? I far prefer to teach memoization first and teach dynamic programming as a kind of optimization over memoization, right? Because memoization is like, reveals the structure of what you're trying to do very, very clearly. It says, look, you've got a problem. The problem has lots of repeated sub-problems. And the key thing is all of those sub-problems are functional, right? Because if they give different answers each time, you can't memoize or dynamic program, right?

[35:50] So I'm gonna have lots of sub-problems. They're gonna be repeated. And each time they're gonna produce the same answer. And because they're gonna produce same answer, I don't have to recompute them each time. I could just stash the answer, right? And now I've got a space-time trade-off. I either choose to stash or don't stash. If I choose to stash, then I'm gonna spend space, but I gain a lot of time. If I choose not to stash, I'm gonna spend time and save space, right? Essentially, that's the trade-off here, right? And it's very clear to explain with memoization. And then you can say like, okay, but now if you look at the structure of the memoization problems, there's this like interesting duality that if you really stare at the structure of memoization, you realize there's actually a trade-off. Like, do I wanna check whether I've already solved the sub-problem or not? Do I wanna compute bottom-up or top-down? Like, you know, memoization is a top-down depth-first process, so you can ask, well, what if I wanted to work bottom-up instead, right? Well, you're gonna have to rewrite your problem to express it bottom-up. But if you do it bottom-up, you can go bottom-up breadth first, and that's called dynamic programming, right?

[36:53] And there's some really interesting trade-offs between those two approaches. And in fact, you can ask an interesting question, why can't I go bottom-up, you know, depth first or top-down breadth first? Why don't those things have a name? And it's an interesting thought exercise to figure out why those things don't have a name, why they don't seem to exist, right? But that's a case where if you approach thinking, teaching algorithms from a PL perspective, memoization is the natural way to think about things, and it really reveals the structure of what you're trying to do, which is you're trying to avoid re-computation by storing the value of sub-problems. That's the essence of the idea, and memoization falls out for free, right? And then if you realize, no, no, no, no, memoization has some performance characteristics that I don't really like, then you can do the work to rewrite this dynamic programming, but then you can use your memoized version as the oracle to check that you got your dynamic program right, right? But that's like, you know, most algorithms textbooks go straight to dynamic programming. And it's always like, it's always a two-dimensional problem. It's always like a two-dimensional matrix. And so, in fact, you can do this.

[37:55] You can go to like LLMs, you can ask them about like dynamic programming, they'll immediately start telling you about the matrix. What matrix? Where did the matrix come from? Why are matrices tied to dynamic programming? There's no connection between the two. It's just that all the canonical examples you see in textbooks happen to have like two parameters that are usually like stringy things or string array type things, you know, like Levenshtein distance or whatever. And so you naturally come up with a matrix in the dynamic program version, right? And so somehow this is associated matrix, but it's complete nonsense. It's utter nonsense, right? And so, it takes a lot of effort to realize the essence of it, which is repeated sub-computation that always produce the same value, therefore you can do a space-time trade-off, et cetera, et cetera. So that's an example where I think like how you say it actually really does matter, right? And if you'd written something recursively in the first place, then memorization is the natural thing to try, right? You have to rewrite that recursive solution, which might be the more mathematical solution into an imperative solution just to get to the dynamic program, right?

[38:57] So there, how you say it does matter. It's not just what? - I wanna push a little bit more though on this idea that you're kind of implying that it's a total historical accident that we've all arrived on the small, you know, implicit programming model. There's kind of a reason that you had the lambda calculus and Turing, and it was Turing's paper that everybody saw and like, oh, that's computation. And that was the solution. - Yeah, but hold on, hold on, hold on. There are two different comments here, and I'm gonna agree with one of them and not with the other, right? So the distance from small to Turing is so great that I don't buy that. I don't buy that like small is the only place we could have ended up from Turing, right? I do think there's a reason we historically converged on small, which is I think it's actually a fairly comfortable programming language, right? It's the reason why like, you know, the type, whether it's typed or not is a separate question. I realize given the name of this podcast, I have to be careful what I say. But setting aside the types part of it, right?

[39:59] Like programming in languages like OCaml or C# or, you know, JavaScript or something like that without all the weird and wild parts. It's actually a fairly comfortable experience, right? Like here's the thing, here's the thing. One of the things that I point out is like, small is deeply embedded in our algorithms because if you think about the cost model behind big O, it is assuming small, right? For example, the idea that function calls take constant time. Any time you do an algorithm analysis, you never even ask the question, how long does the function call take? That takes one unit of time. You assume some constant number of parameters and it takes, you know, a bounded number of parameters. It takes a constant amount of time, okay? Well, how is that possible if you copied arguments? If you copied arguments then it's gonna be dependent on the actual argument size, right? So the very fact that we assume that function called take unit time means that we must have assumed that we are not gonna copy the values to parameters. We're gonna pass references to them.

[41:00] Well, that's the small model right there. So you combine that with mutation, you've got small, right there. You've got the core of small, right there, right? So it's deeply embedded in everything. I'm not sure it's like Turing per se. I don't think, I don't, I'm not quite ready to say like, I mean, I don't, I haven't traced the full history here. I think it's certainly the case that if you go to complexity theory courses, there's very few people who tried to do complexity theory through like Lambda calculus. Most complexity theory courses are definitely done through, you know, Turing machines. And that's an interesting question in itself. But I think there's a gap there. And I think that gap has something to do with like, like it's powerful, but not too powerful, right? We've tried, we've tried versions of it where it was more powerful, more powerful. Like we're gonna make, you know, variables first class. So we're gonna make, you know, variable aliasing. And it turned out that turned out to be not such a good idea, right? And so we'd retracted from that till some languages did try that, right? And they're like, oh, it's really important. How else would you ever write a swap function if I couldn't like have variables be aliased? Then we're like, you know what?

[42:02] Swapping turns out to not be so important in contrast to all the problems that like, you know, variable aliasing causes. So we'll allow data aliasing, but not variable aliasing, right? And so we retracted. And so we did end up, after various experiments, we've ended up in this reasonably comfortable space. So I think it's not a bad design. I think it's a pretty decent design. - So in your experience kind of teaching to, you've taught all levels of undergrads, including like first year undergrads, correct? - I do everything from first year through PhD students and through bootstrap indirectly, work all the way from middle school. So my scope goes from like, you know, roughly like 10 to 12 years old to like do infinity, I guess. - And you've tried both teaching them with a kind of small type of model and with the Lisp first model, right? Have you had a comparison of the two? - I'd never done small first. I've never done like mutation first. - No, not mutation first, I guess, but like of a pirate style. - I mean, scheme is small. So small is just a funny name for scheme.

[43:04] - That's right. - You know what, that was, that's on me for implicitly. - No, no, no, it's fine. No, no, but there are questions like, you know, how early do you bring higher order functions into the mix, right? And I've certainly so like, you know, DCIC, the data center construction computing actually brings higher order functions much earlier, right? Then like how to design programs does. And I think you can get away with that. And actually I sort of exploit the fact that novices tend to focus on superficial aspects, right? Because if they didn't, you know, there's always like the student who doesn't, but you know, most of them, like you say, look, you know, you just do this and you give it this thing as a parameter. And they're like, yeah, sure, I'll give this as a parameter, it's fine, right? There's always the odd students like, wait, is that, isn't that like a function? I'm giving a function like, shh, okay, all right, okay. That is what's going on, yeah, that's what's going on. Okay, good, good, good. Just wanted to make sure, yes, right? And the rest was like, okay, fine. I just had to put a name over there. I put the name of a function and it's a named thing, right? It's a named function. And so like, is it that different from a named variable? Who really knows, I'm not thinking that hard, right? But you can take advantage of that, that they don't ask too many questions and you can actually start doing higher order stuff much earlier as a result.

[44:15] - So you see them as equivalent, right? You wouldn't, do you have a kind of dominating philosophy on whether we should teach first year undergads, a schemy type of thing, a parenthesis type of thing, or a pirate type of language? - Oh, I don't think I, look, look. I was exposed to sick be my first semester in college and was a life-changing experience, okay? It was amazing. So it's a structure and interpretation of computer programs, abelson and Sussman and Sussman, okay? Amazing experience. I think that book, I think that book it, you know, it has the statement like don't assume that this book is for certain kinds of students. It is completely false. It is absolutely only for like certain very, very nerdy kinds of students. I remember as an adult going back and saying like, you know what, I seem to remember like data structures showed up fairly late, like how did the book, what did the book do for the first like 30 pages? So I went back and reread the book, it was all like, you know, number theory and like electrical engineering, like who's your audience here, man? Like, you know, come on, right?

[45:16] So it's, to me, it's like one of the true, I say this with no sense of irony and with the most profound respect. I think structure and interpretation of computer programs is one of the great works of literature. It's one of the great books of humankind. I mean that with no, I absolutely believe that. It is a mind bogglingly great book, but it is not a book for everybody and at all in the slightest, okay? So setting that aside, so I saw the power of that, but I'm not sure that I would necessarily use scheme for most beginners. I think we built pirate for that reason, right? Because I don't want to have the debate about syntax. I want to get to the ideas. And if we constantly sit there talking about syntax, we'll never get to the ideas. - And is that debate about syntax come from, like, students' prior expectations about what a programming language is supposed to look like? I thought it was kind of pressure from external, the external world. - Yeah, I mean, you know, we get a lot less pushback like middle school students. We get a lot less pushback from math teachers, right? In fact, like, you know, Bootstrap, one of the Bootstrap curricula, exploits the parenthetical syntax in a very deep way, right?

[46:26] It's like trying to teach, it's teaching students about like order of precedence and stuff like that. And we actually like take deep advantage of like parenthetical syntax. It's central to the curriculum in a certain way, right? To that particular curriculum. And the teachers, the math teachers love it. They're like, oh, this is great. Like, I, you know, this is so much better notation. The students don't question it, right? So it's clearly like this, this, now, of course, they're writing fairly small programs. So maybe if they wrote like, I don't know, a thousand line program, so they had 17 parentheses closing off or something like that, maybe it'd be different. I don't know, okay? But it's certainly to some extent, at least an acquired thing, right? It's certainly something about like, what does the world expect? And is this weird, et cetera, et cetera? There's, again, you know, I said there's emotions, but there's like society and like education is a very, very complicated business, right? It is not like, it is not at all a simple rational model of like learner and teacher or anything like that. - Let me grab you right there. I was meaning to ask you. So yes, education is a very complex business and it seems to me that you have spent a lot of time and effort trying to understand the best ways to educate about programming languages, about programming in general.

[47:38] And so my question here is, what's your education philosophy? What do you think and what is your experience that works best? And it also seems to me that you spent a lot of effort teaching how to design programs. So why do you think that's so important? - So let me say a little bit about my philosophy. I think I do have, it took me some time to articulate a philosophy, but I do have one. I think one of the things academics are really good at is producing clones of ourselves. Okay, we go into a classroom, we teach, we do our thing, and then, you know, we get some feedback. Most students, I don't know, they don't say anything, they seem fine, they do okay on the test, whatnot. You know, if I'm being really sarcastic, I would put it this way, right? Like if the students do really well, I'm like, look, I mean, I'm such a great teacher, of course they're gonna do well. And I do badly, you're like, what can I do? Look at what I've been given as students, like, well, I've done my best, right? So, I mean, I'm being a little sardonic, but not entirely, because I've heard these kinds of things, right?

[48:43] To be fair, I'm not saying like, it's easy, you know, sometimes the best of our efforts don't get through to students, it's okay, right? But I think we do have this danger of academics in general of like creating our clones. And so the feedback we get is from the students who are most like us, and they're like, oh, I love this course, it was amazing, it was just like life-changing, you know? Your book is like one of the great works of literature, blah, blah, blah, right? And we don't hear from the rest of the students, right? But I had a moment of insight, okay? So my moment of insight was, I was talking to one of my advisees at Brown, and I tend to attract students, my advisees tend to be students who might be more interested in PL-ish stuff and things like that. And I had this, you know, and so some of them are also like very like anti-machine learning and stuff. They're like, oh man, like I just wanna like focus on fundamental stuff, blah, blah, blah, you know, stereotype a little bit there. So I had this student who was like, I really take machine learning, I said, look dude, you really should take a machine learning course. Like I just, you just gotta have like these tools in your tool belt, you never know when they're gonna come in handy.

[49:49] It's just like having more tools in a toolkit is always good, might be useless. Take one course, if you're an undergraduate, getting an education, just take a course. Oh, which one? Machine learning, deep learning, whatever, we have like a bunch of these courses, it's okay. And I thought about this experience for a little bit and I said, you know, what am I hoping from that course? I'm hoping that that course is a service course, meaning there are more advanced courses, right? But that introductory machine learning course, intro to machine learning or intro to deep learning or whatever, is gonna not assume that every student in that room wants to become a deep learning researcher, right? It's basically saying, you have come, you want to get a basic toolkit in the subject, we're gonna give you a basic toolkit, we're gonna drop various pointers to more advanced stuff, we're gonna have like, you know, supplementary material. If you are serious about learning more, you can come and talk to us, but we are gonna provide you like a basic service that is useful to you that you can take away from here and go do something with. Okay, so if that's what I want from the machine learning course, what is the job of the PL course?

[50:53] Why is it not the same, right? Why should I not, shouldn't my philosophy be that there's some student out there who's really into machine learning, right? But they're like, you know what? I've been told that like, I should take PL, I'm told that it's like sort of a useful thing, I should know something about, and you know, Sherm keeps telling us why we should all take like a PL class. So I guess I'll go take his class and see like, what am I gonna learn? And if they come in and what they're taught is basically like, you know, a graduate grad level PL course, what are they getting out of it, right? So that's part of the 90% philosophy. And again, you know, when my colleague Tim Nelson and I designed our formal methods course, which he's done amazing stuff with one of our two formal methods courses, we have two at Brown now at the undergrad level, but we're, again, we're gonna consciously design this course for the other 90%, right? We are gonna, because the 10% that are like us, it sort of doesn't matter what we teach. It really doesn't matter, right? They will take, they will lap it all up, they'll come to our office hours, they'll come and ask for more, they might get a little annoyed that we didn't teach like the most theoretical version of the course or something like that, but they'll go to grad school, they'll take the course, I'm gonna write the letter for them, they're gonna go to the grad program of their choice, they'll take the course there and it'll be just fine, okay?

[52:08] But that other 90% when they come to a formal methods course or a PL class, I wanted to go away thinking like, this course spoke to me in some meaningful way, it told me something useful that I can take to my job as a programmer or whatever, right? And that's the kind of course that I wanna design and I think that was, that's my philosophy, right? At the undergraduate level, at the grad level, now, grad level, we're gonna teach, we're gonna go all in, it's a pure theory course, we're gonna do the theory, we're gonna do like, we're gonna do the proofs, we're gonna do all of that stuff because I'm training you to become a part of the discipline, right, but at the undergrad level, that's not what I'm training you for. So I think that has driven a lot, yeah, sorry. - And what exactly would you say you would like for them to take from the course and use in their jobs exactly? - Well, so I think one of the things is, so I think there are two sort of, okay, so in my old PL class until this year, which I'm redesigning right now, right? Roughly speaking, I wanted to do two things. One is having spent a lot of time understanding the, doing research on misconceptions of small, right?

[53:15] Given that they're all gonna be programming in small, given that they have all these misconceptions, I want to help them correct those misconceptions. That's one goal, okay? A second goal is, I want them to understand like the, I wanna understand like, where do languages come from? Where do language designs come from? What have we historically done and why did we do those things? That's the second goal. The third goal is, I want them to be able to write, like implement the essence of some of the important ideas, the essence of an implementation, essence of a type checker, essence of maybe type inference, things like that. So they get a feel for like, oh, these aren't such mysterious things. I can build one in a week myself, right? And then the fourth one is, I want them to be able to relate the concepts they're learning in the course to the broader world of programming, right? So reaching out to the broader world of programming and reaching out to like things, phenomena they might see in the world, phenomena from languages that are not discussed in the course and so on and being able to relate from here to the broader concepts. So I call it a multi-threaded course.

[54:16] There are four threads to the course and one thread is like the standard model thread. The second is this thing that I call mystery languages. The third is the implementation track at the thread. And the fourth one is like what I call the analysis thread where you're like relating things to the world. Like, here's a tweet. Here's a problem that somebody posted on Twitter. What's really going on, right? You should be able to explain this in terms of the length of vocabulary of small, right? Or here is an article about the design of goal routines or something in goal. Let's try to relate it to something we saw in the course. Or let's think about the design of error messages, right? Or let's think about language, natural language, like why are all of our languages English-centric? What if we had like, you know, in fact, you know, one of their jobs is to build like a language where all the keywords are in Spanish instead, right? So they build like a baby racket with Spanish keywords and say, or any other language of their choice. One of the students who took the course but then built a version in Thai because his mother doesn't speak any English and he wanted to teach her how to program. So he has a version of racket where all the keywords are in Thai and you know, I can't read a word of it. And that's wonderful. (laughing) - That's awesome.

[55:19] You gonna say something, Dan? - So what is it, you kind of talked about like wanting your course to be like, that it should be of service to those students who aren't necessarily interested in programming languages. But is that like, is that the thing that motivates you to reach out to those types of students who are not the top 10%. - Oh, I wouldn't say, hold on, I'm gonna correct. I'm gonna be a little picky here because it's not that they're not interested in programming languages. They're not interested in becoming programming languages researchers. If they're not interested in PL, like they're not gonna take my course. It's not, I'm delighted that PL is not a required class. I don't want it to be a required class. I'm delighted that the students who come come because they have some interest in doing something, right? So they're interested in, they're at least intrigued. They're not necessarily interested, right? It's my job to cultivate interest, right? But they're at least intrigued, right? And this is actually why I also stop doing like mastery learning kind of things, right? Like for the 10%, like mastery learning makes sense. For the 90%, like I'm not sure that's actually the right, that's the right criterion, right?

[56:20] I want them to be competent as opposed to necessarily masters. - Mastery learning, that's where you break your course into individual units and you have to get 100% perfect in that unit to get credit. - You can't, yeah, essentially, essentially, essentially, essentially, right? And in fact, there are, in fact, you know, at Brown, we have this like pass fail mechanisms. You can take courses pass fail. And so I say, look, if you're gonna do pass fail, you're welcome to, if you're doing pass fail, I actually, there is no value to me. So this is going back to the mastery learning in a funny way. There's no, I am not interested in you getting 50% across the board on every assignment. I would rather you get 100% on these assignments that I think of as essential, right? Like if you're 50% across the board, that means you're just like bad at everything, right? But instead, I'm just gonna say, these are the more advanced assignments. They're for the students going for the letter grade or for the, you know, for the 10%, right? But if you just wanna take the pass fail version of the course and you wanna get like a baseline in programming languages, these are the essential assignments.

[57:21] These are maybe the more out there, more whimsical, more like setting you up for future study assignments. You don't have to do those, just nail these, ignore those. Don't even spend time on those. I don't want you to get, there's no point in you getting 10% on those, just nail these other assignments instead, right? So I think there's value to thinking about like, what are the essential things I want everybody to know, right, versus what are the things that like, you know, the more aspirational topics that I wish everyone knew, but I don't feel like is absolutely essential. Like type inference versus type checking is a good example. Type checking to me is an essential topic. If you're gonna get a graduate of PL class, you have to be able to write a working type checker, right? But type inference, Hindley Miller type inference, not that important, right? I think it's one of the most beautiful algorithms in the history of computer science, but that doesn't mean like everybody should have to study it and everybody should have to know it. - This is starting to get a little bit into pedagogy stuff, but isn't it like, I mean, what you're talking about is ideally you would have students who are comfortable with getting a C and then just going along with it, but everybody wants to get an A, they have to get an A, so they have to do all that.

[58:28] - Not if you're taking the course pass fail, not if you're taking the course pass fail. - Oh, it's the pass fail, but who takes the course pass fail? You already have to. - I think that's the biggest misconception then, because, and I really relate to what Shira is saying here, because I see a lot of professors failing to take into account this great amount of students that don't really care about the topic, they're just there to get along, like to know what is going on, and they're not really interested to go deeper, and they will not, there's nothing the professor can do to motivate them to go for a great letter grade, right? And it's okay, and it's fine. - I mean, just even this thing, there's something in computer science almost certainly that you're not excited about. Maybe it's machine learning, maybe it's graphics, maybe it's something else, right? And let's just imagine you're the undergrad who's like, you know, I'd like to know a little bit about that. This is an opportunity, right? I'm here in college, there's somebody offering a course in it, I have no plans to ever go to grad school in it or work in that industry or anything else, but I'd like to know something about it, right?

[59:32] I'd like to be like educated about it. That was why I came to college, to be an educated person. I, you know, in my case, for example, I know nothing about graphics, like even ASCII is like a little complicated for me, right? So I don't know nothing about graphics, but so that's the subject where I might be like, you know what, everybody tells me it's amazing. Everyone says, oh, ray tracing is this like amazing algorithm, which I believe because I have a graphics colleague next to my office who comes and talks to me all the time about it and convinced me about its beauty. But let's say I didn't have the benefit of like, you know, the author of the world's best graphics textbook coming into my office and explaining things to me, but instead I'm a student at the university. I'm like, I'd like to take a course and find out like, what do graphics people think about and how do they think about the world, right? I think I should be entitled to that course without having to want to become a PhD student in graphics. - Yeah, and the question was just how, what makes you interested in that student? - Oh, because it's so easy, because that's what makes teaching challenging. It's super easy to teach to the student who's like me. It's trivial, I mean, I can, again, the other thing is I can teach anything I want, it's not gonna matter, like anything I eat a thumb, they'll be like, oh, great, show me now.

[1:00:45] It doesn't matter, right, there's no challenge in that, but then I'll have like, you know, a much smaller class and it'll be amazing because every student in the class will be like a mini me, but I mean, that's my grad course and I'm very comfortable with that in a grad course, right? But I think like that's not my job as a person teaching an undergrad class, literally not my job, that's not what I think my university, I don't even know what my university expects of me, but that's not, my university should expect this of me. - I think Sri Ram is also from a university where there is not, I'm assuming here, but I would assume that there is not too many bad students in the sense that they struggle too much with their topics. - We have a spectrum of students, okay? It's certainly the case that, you know, Brown admissions is competitive. We do have a spectrum of students and you'd be surprised by what students might struggle with. And I think, I mean, look, look, I am gonna be really clear, I am extraordinarily privileged to be working at Brown, right?

[1:01:46] It's an amazing place and I'm super, super, super fortunate, like a whole bunch of things, very surprising things, luck fell in my way in lots and lots of ways, dozens of times in my life for me to end up where I am. And I'm super privileged, I don't dispute that. But I think there is also a danger in assuming that somehow like, oh, these students, you know, they can do anything or they're like all motivated, they're all interested. And I don't think that's true. And again, as I said, even if they are, they might be motivated by something else, not your thing, right? They're not that interested or that, you know, previously able or whatever in your thing. That's what matters the end of the day. And that's gonna be true wherever you are. - In any case, the argument I was gonna make is that it's always so fulfilling to be able to really help a student who wants to get across your subject and is just not able to. Like you can see in their eyes that they're trying and they're not able to. And if you just give them some time and sit down with them and explain things in another way or a slower way, they can do it, you know, like there are, sometimes if you don't just need someone, someone to just like give them a little push and only be like, hey, calm down, just let's just break this down and you're gonna get to the other side.

[1:03:02] Sometimes that's all they need and it's really-- - Tutoring, tutoring is, yeah, yeah. But you know, Dan, you were asking this question, right? I think there's another thing for me which is, I think PL is just one of the most beautiful things in the world, right? And I want as many people as possible to see the beauty of it. It's just fucking beautiful, man. Like it's just, it's like, I am just happy when I walk into a PL class. I'm just happy that I could, like I'm, I feel like lucky to have been born in an era where this thing exists. Like if I were born in like, I don't know, 1920s, I'd have been like a terrible physicist and I'd have missed out on all of this beauty, right? And I'm fortunate to have all this beauty at my fingertips and be able to pass on some of that beauty to other students and hopefully inspire them, right? I think programming language should be inspiring. You know, you were talking at the very beginning, you were talking about like, you know, trying to enable things versus like disabling things, roughly speaking, right? Like preventing things. I think we spend too much time in PL worrying about like preventing things and not enough time about like enabling things, right?

[1:04:06] I like to give, you know, I like to demo in class. I do demos of like, you know, FatherTime or of like Prolog. And I like, there's the student, you know, you see like eyes light up like, I didn't know a programming language could do that. And it's like, fuck yeah, they can, right? That's the point. Like we gotta inspire them to say like, the limitations of what you've seen are trivial. We can vent anything we want. Let's go out and do it. You know, like that should be at least half of the goal of a PL class is to say, look at what we can do and look at what we've done. You're sitting there wallowing in the mire of like Java or something like that. Well, look at what we had in 1972. Come on. - I love that. That's beautiful. - So I think we have to, I think we have to like also think of like our classes as like bringing in these students who've never imagined any of these things, who've been to like, you know, these pedantic like Python and Java programs and inspiring them and say like, there is a much more beautiful world out there.

[1:05:10] (laughing) - Yeah, I love it. I love it. That's great. Thank you so much. That is very inspiring. And I definitely relate to that. Yeah, I also really love teaching and you just took the words out of my mouth. And I think that's one of the things. - You know, there's the famous Petrarch quote, right? There's the famous quote from Petrarch. The mind is not merely a vessel to be filled but a fire to be kindled. - Oh, we gotta like kindle the fires. Yeah, you gotta go in there and kindle. - I wanna come back to this afterwards when we started talking about AJTIC programming because we still have a lot to talk about and an education about that. But before, let's talk a little more about formal reasoning, proof of assistance. And even before that, why Racket? - Oh, why Racket for what? - For teaching, for doing like what do we do with Racket? Like what is Racket? Like can you teach us, like tell us a little more. Like you've mentioned Racket a couple of times and I've never had anyone who I could ask this question. - Have your program in a shell script?

[1:06:11] - Yes, it's disgusting, I think so. - What's the first thing you do in a shell script? What's the first line? - Tell you what is the language of a bang or something. Where is your program? - Yeah, you say like hash bang, hash bang, bin bash or hash bang, bin CSH, right? But you can also say like hash bang, user local bin pearl or whatever, right? That's actually, it's called the shebang, right? So basically the first line tells you how to interpret all the other lines, right? So it basically says, there's nothing that actually says a shell script must be in the shell language. The first line determines the semantics of the rest of the file, right? - All right, yep. - Okay, Racket follows essentially the same principle. The first line says hash lang, followed by which language is this in. And both the syntax and the semantics of everything that follows is determined by what you say after the word hash lang, okay? So there are lots of parenthetical languages in Racket, but there are also completely non-parenthetical languages in Racket.

[1:07:19] There are typeless languages in Racket, there are very typed languages in Racket, right? So I do a lot of my programming, for example, in a language called plate, which name is not interesting, but I work in plate, which is basically standard MLs type system in Racket, okay? Or gradual typing was co-invented in Racket because it was easy in Racket to create like a gradually typed language as opposed to like a purely dynamic language. There are Racket languages that are, like there's data log, with data log syntax is a Racket language. There are some languages that have like a data flow semantics instead of like a small semantics. There's scribble, which is an amazing language for writing documents where you write like essentially markdown text, right? Like not quite markdown, but like markup, let's call it markup instead, markup text. So you say hash lang scribble, and if you say hash lang scribble, the rest of it is actually a text file with markup in it, right? So the point of what Racket does is it's sort of two things. It is a particular programming language that is like a small language with like objects and classes and all these other things.

[1:08:22] But it is also a machine for defining languages so that the first line, just like in a shell script, determines what the rest of the file is, what language the rest of the file is, not only semantics, but even the syntax. So it is a language that is designed for building languages, okay? Now, the reason I use it in teaching my PL class, now, as I said, we have these multiple tracks, right? So I need to define the way my pedagogy has been defined until now is I need lots of different languages with different semantics, not so much syntaxes. I keep the syntax as pretty uniform, but I make some small syntactic changes to avoid people getting confused about which language we're in, but I need lots of different semantics. So, you know, one of my illustrations is I have this thing called the mystery language approach where I'm trying to teach you about, you know, so the way the course is structured is we sort of go feature by feature, but inside each feature, I want you to understand that there's semantic variation and what that feature might be, right?

[1:09:24] So we have like, you know, we say object, but object means like a half dozen different things, right? We say even number means a bunch of different things, like is it exact, is it inexact, is it rational, is it floating point, whatnot, okay? So in a mystery language approach, what we do is we say, I'm gonna give you a syntax, I'm gonna give you like an informal English description of what the syntax means, and so now you can write programs in it, right? So let's say you say five plus seven, right? It doesn't print 12, it actually prints 12 three times. It prints 12 three times because there's actually three different implementations with three slightly different semantics. So your job is to come up with a program that tells the languages apart. So you know what the operations are, try to figure out like basically it's like an adversarial thinking exercise, you go and try to figure out how to tell these apart, right? So for example, if you say one divided by zero, one of them might give you, I don't know, like one of them might say error, one of them might say zero, and one of them might say undefined, right? So, or if you say 0.1 plus 0.2, one of them might say 0.3, the other one might say 0.3004, right?

[1:10:31] So your job is to tell the languages apart, and we do this as a bottom-up activity, followed by the top-down activity where I tell them, look, each of these languages, some of these are really weird in their semantics, but each of these has been designed by me to be a real, it represents a real language either now or previously in widespread use. So this is not like me making up weird semantics. Large numbers of programmers have had to, or maybe even now do, deal with this semantics, right? So for that, I need like to build about 40 different languages, right there, 30 different languages for the mystery languages alone. Plus, I have, you know, languages for doing other things. There's a language for like enabling you to write garbage collectors without having to write implementations of languages. All of these things, I need like, I need a very fluid medium for defining languages. In some cases, defining languages for defining languages. And that's what Racket gives me. That's why Racket. So it's an ecosystem of languages. It's not one language. We don't actually, the only language we don't actually use in class is #Racket.

[1:11:36] That's the one language we don't use. We just use a whole collection of specially designed languages for the purposes of the class. - So if you were kind of designing this class today where code can be very cheaply made with, you know, codecs, these agents and stuff, you could potentially remove the Racket middleman altogether. Not saying that you would want to do this, but your point is you want to make a bunch of different languages that, and a bunch of different compilers, a bunch of different interpreters, and you want to show those things and them to be kind of similar to something that exists in the world, but similar enough to one another that the students don't have too hard of a time jumping. - The more importantly to one another, more importantly to one another, right? Because, in fact, all of these languages have a parenthetical syntax on purpose because once you've picked up the parenthetical syntax, you don't have to spend any more time thinking about the syntax, right? It's not like, oh, is this gonna go to the left? Is this gonna go to the right? Which has the higher precedence, lower precedence? None of those things, right? Now, there's some ways around that. There's a new language, Matthew Flatt's design, called rhombus that might enable us to do the same thing with infix syntax instead, so I'm investigating that.

[1:12:44] But it's the same idea, right? Hashlang, you define the, you give, you tell me what the language is. The syntax, the key thing is less that it relates to things outside because people don't program in parenthetical syntaxes. It's more that once you're inside this family, we can study variations. So this is like based on stuff in cognitive science, right? People focus on differences, and so you wanna study variation. And to study variation, you wanna keep all the unimportant things the same because then they can focus on what's different. So for example, I have, you know, in objects, I have a thing that roughly reflects Java, roughly reflects Racket, and roughly reflects like JavaScript Python. JavaScript Python Ruby, Racket, and Java, okay? Java C#. Okay, now the problem is if I gave you actual Java C#, the programs would look completely different, right? And the ecosystems would be completely different. And there's all this other noise of like, you know, and you have to write class in one language, you don't write class in the other language, you have to get three different implementations, and all of that noise would completely drown out the point I'm trying to make, right?

[1:13:50] In contrast, here I'm giving you one syntax and three different implementations for that same syntax. So all you have to do is you get like a language with like six constructs, and within that, you have to be able to figure out what's different. You drill down to the essence. And anything that would let me do that is great, but Racket lets me do this amazingly well, so. Don't forget what podcast you're on. We already can do this. You just have monads. You have a monad for every single programming language, right? So in a way, does it all come down to syntax? Like, could you just as well have done all this stuff with monads? The only difference is that like, I don't wanna have to write the stupid angle bracket and then asterisk thing to get the monad to work explicitly. - I suspect a chunk of it probably. I mean, like some of it is not even monadic, right? I'm just parameterizing a syntax. It's not even, there's not even like a, I don't even need monadic variation, but the point is I don't have to think about the machinery because I get to control all the machinery behind the scenes, right?

[1:14:52] And because I'm also coming from a very full featured language with side effects and everything else, like one of the key things is that every time we do these mystery languages, one of the languages, there's always two to four languages, one of them is always gonna be the small semantics, right? So there it's just like, you just literally get racket. I mean, or some sort of skinny core, whatever, right? That's what you get. And that the others are defined as a variation on that. And it also helps me audit to confirm that that's the variation that I wanted, right? I can look at the diff, the semantics files and audit confirm that that's the diff that I wanted. You could do this through other mechanisms. I'm not saying you couldn't. It does mean that I can make the surface language as minimally noisy as possible. But also I get to define, here's the other thing, right? I get to throw things out of the language that are not relevant or that might make mess things up, right? Like you don't have a, with Monads, I can parameterize a thing, but I can't say, and don't give me any of the rest of the language, right?

[1:15:58] I'm creating sub languages, like very small sub languages. In fact, the first, the illustrative example we do is a string language with just strings. All it has is string constants and string concatenation. That is all it has. There's nothing else. If you type three in the language, it says, I have no idea what that is, right? And that restriction is also important because it ensures that there isn't gonna be some other weird feature that's gonna interfere. And then the students think that's what we're trying to focus on rather than thing we're actually trying to focus on. So it's the syntax, the language restriction is just as important as everything else. - That's a good point, yeah. - It's not a convention. It's an actual, it is the whole language. It's not just a, by convention, please don't write the following things, because that never works. Students never, ever understand these conventions. They always screw up the conventions. And the thing is, I'll just point out from a pedagogical point of view, it's fine. I can say like, well, you screwed up. You used a thing you weren't supposed to use. You're, you know, no credit for you, right? But my goal here is not to be punitive, right?

[1:17:03] There's a deep learning objective here. And the key thing is not that they get zero credit. The key thing is they didn't obtain the learning objective. The thing I wanted them to learn, they did not learn because they got distracted by some other thing in the language that they were not supposed to. And they forgot in the heat of the moment, oh, I'm not supposed to do that because nothing told them they're not supposed to do that. Nothing's checked, right? So that's the problem with conventions. People forget. But the result is they don't get the learning objective. And my goal here is not to give them zeros. My goal is to like get them to learn. - Yeah, I actually totally agree. And I come from that tradition as well, personally. I think it's just the interesting thing to me is like, you could, how well the things that you're talking about actually map to something like Haskell, which in a way that I hadn't expected until you just articulated them that way. But I think that the real difference comes down to that aspect of it, sure, like a bit fewer foot guns, but also this aspect of like syntax is so simultaneously important and so irrelevant at the exact same time.

[1:18:14] And it's hard to kind of square those two things. I think for beginners, obviously, like you mentioned that the superficiality in both senses is very important. But it's also what kind of we love about Lisp, right? The fact that it's home iconic, for example, right? Although you have-- - Oh, you don't want to say that word around me, buddy. (laughing) I'm not gonna take that bait. Okay, moving on, yeah. - Okay, okay, okay. - Yeah, I have a blog post for you, yeah. - Oh, there's a blog post for everything. It's like, Shroom is like the XKCD of blog posts. - I have like seven of them, man. You're just hitting all of them, that's all. No, no, but setting that aside, the point is the syntax is simple. And look, I wanna be really clear, right? I'm not saying that I can't do this in some other language, right? I am biased because like, bracket hashlang is the mechanism. I understand the best, right? And it's the least foot guns for me, which is also important, right? So if somebody wanted to say, hey, I've taken all of the ideas from Mr. Languages, you know, we've got papers, we've got the whole repo online.

[1:19:20] We've taken the whole idea and we've done this in whatever other language. I actually suspect it's probably, there's certainly a version of it you could certainly do in Lean. I don't know how to limit the language in Lean, but certainly with Lean's macros you could do a lot. I don't know how to limit the language. That's the other part, right? The limiting of the language. So the fact that I wanted to be able to completely define the constructs in the language, right? Limit it and not have students write in any patterns, right? Those were two like non-negotiable conditions for me. And in Racket, I knew how to do that without any difficulty, right? And maybe if somebody else can show me how to do it in another language, I would love to see it. It would totally delight me to see it done in some other language. - Moving to another, to a different topic a little bit. I see a lot of professors, I see a lot of courses focusing, when we're talking about programming languages, they want to focus more into the theoretical part, specifically formal reasoning, maybe some proof assistance and start getting a little more into type theory. What are your thoughts on that?

[1:20:23] Do you think that's going too far too fast? Do you think that's a wrong approach to go into? - That's super important, super important. I just think that you have to find the right place for it. And I think maybe where I disagree with some people is where is the right place to do that, right? I don't do that in my undergraduate course, but I think that's what my graduate courses do. So, I make a very hard distinction between courses that are designed for the 90% and courses that are designed for people who want to become part of the academic family and learn how to read a POPL paper and then write a POPL paper or read a PLDF paper and write a PLDF paper. - You don't think it's possible for the 90% to appreciate proof assistance? This is a type theory for our podcast, I have to ask this. - Good, I will tell you what I think then, okay? I actually don't think most people care about proof. - Okay.

[1:21:25] - That is my heartfelt opinion, okay? Now, I actually do care about proofs. I have done some pretty massive proofs. I really care about knowing why something is true and being able to prove that it's true. But I think for the vast majority of people, look, it's hard enough to get people to care about whether something is even true. Forget about proof, okay? It's hard enough to get people to care about whether something is true. Now, I would argue that if you're gonna be in the discipline of computer science, you should care about whether something is true or not, right, like you shouldn't be, oh, I think this is a linear time algorithm and it's actually a quadratic time algorithm. It's a pretty sucky thing for you to say as a computer scientist, okay? And so, analogously, I think this thing is sound or this thing is safe when it's not is a pretty sucky thing for you to say, okay? So, I think we should care about truth. But we know that, you know, we know from logic that truth and provability are two different things, right? And similarly, truth and proof are two different things. So, caring about truth doesn't mean that you care about proof.

[1:22:29] And I think we conflate those two in PL and, you know, I've had the benefit of having a much broader education and formal methods than I think most PL people do. I, you know, I studied with Moshe Vardy when I was a grad student and he was, you know, I took like all of his grad courses and I was like deeply steeped in computer aided verification from Moshe's view of the world, right? And I sort of learned like three things from Moshe, right? One thing I learned is everything is finite model theory at the end of the day, okay? The second is I learned about model checking and automated methods. And the third is the thing that Moshe taught me also is what matters is less proving things correct and more about finding bugs. At the end of the day, the real value add comes from finding bugs, right? And I also was very deeply influenced by Daniel Jackson. And what Daniel taught me was like you, before you invest a lot of time in knowing, in proving something, you should have a sense of whether it might actually be true or not, right? And we don't have very many tools for that in our toolkit. But if you step outside the PL toolkit, I mean, I think some of these ideas are starting to come into PL slowly, right?

[1:23:36] But if you step outside PL, like things like model checkers and model finders and like, you know, like lightweight checkers are all over the place because people want to know, like they wanna, look, it's even less that we care about truth. What we care about is gaining confidence in things, right? I think we have this like very misleading view of the world that I'm gonna prove a theorem about it, therefore it's true. No, no, no, no, you're gonna prove a theorem about a model of a thing, okay? And it's very rare that you prove a theorem about the thing. And that model is now where all of the bugs are lurking. And that model was almost certainly a simplified notion of reality so that you could fit it into whatever axiom system you had. Now, I see this as somebody who has done this, okay? I wrote one of the first type soundness proofs for Java back when there was a question where the Java was type sound. I've done, you know, I've done security theorems, I've done soundness theorems, I've built type systems and proven them sound in pretty sophisticated ways. I played the game because I believe in it.

[1:24:39] I truly believe in it, right? But I also know in the process that when I prove a soundness theorem, the soundness theorem is relative to some model of the world. And we have to always ask, is the model an actual statement about the world or not? And most of the time our models are not, right? And that means we haven't actually proven a thing about the thing. We've only proven a thing about relative to some model, right? And, you know, like when we did like our JavaScript work, right, we were like, we said, we need to make sure, this was like Arjun Guha's great insight, was we need to make sure that our model of JavaScript actually matches what browsers do, not what I invent JavaScript to be. I can't just be like, let Lambda X, you know, let me just write some Lambda terms and call that JavaScript because at the end of the day, we're trying to prove security theorems. We're trying to prove like, you know, sandboxing theorems. And if you want to prove a sandboxing theorem, you have to prove your theorem against an adversary, right? I don't know of any adversary out there who's like, oh, I found an exploit, but I see it doesn't fit your model. Therefore I shall be, you know, a proper gentleman about this and not exploit you.

[1:25:43] Like, what the fuck? Of course that's not how anything works, right? So I have a profound respect and I teach this idea of like modeling is a, I mean, like in every discipline, right? In every single discipline in physics and chemistry and mathematics and, I mean, math is itself an abstract. But, you know, physics and chemistry are economics, right? All these disciplines, like in computer science, we make progress by coming up with a model, right? And it's always like, you know, we all know that George Box quote, right? All models are wrong. Some models are useful, blah, blah, blah. But the point is we can get models to be more and less wrong. We can get models to be closer and closer to, we can get models to tell us about the things we care about. But we should always recognize, you know, after the financial crash, Emmanuel Candace and somebody else had this like, what they call the modeler's Hippocratic Oath, right? And the Hippocratic Oath is basically like, I shall recognize that my models are not reality. That was part of the Hippocratic Oath, right? So you can do all this proof against a model, but unless the model is like watertight, you haven't proven a thing about the real object, right? So another thing you can do, and so that's a good thing to do, right?

[1:26:48] You can then stress test your model and discover all the ways in which it may or may not actually represent reality. But another thing you can do is think hard about what people actually want and what people actually want is confidence as opposed to truth. And there's many, many more ways of getting confidence, right? A lot of the work we did on like differential analysis was basically doing semantic differencing because what tends to happen in reality is you have a system and it works. What does it works means? It doesn't mean that somebody sat there and did like a certified proof of it, but it means that like, look, they did some proofs, they did some testing, they did maybe some property-based testing, they ran some test vectors against it, and they've been using it for six months and nobody's found a problem. That is how we gain confidence in systems, right? But then something comes along. Either somebody says, oh, you know, I need this feature change. Or somebody says, I found a bug, please fix this right away. And now what you wanna know is not is the new thing true, you don't even know what truth means. What you wanna know is how can I transfer my confidence in the old thing to the new thing?

[1:27:54] It's transferring of confidence. And that's what we did. We did a lot of work on that problem instead. So we can use all the machinery of formal methods, all this amazing tooling we have, but to ask a slightly different question. And I think we have gotten ourselves trapped into a little maze of twisty pastures where we don't always ask anything other than this one question. And even what we prove, you know, for the most part, we do like soundness, we do like safety proofs, because that's what's easy to do with our machinery, right? But, you know, I started, I said, you know, when I learned formal methods and verification, like we always learn about safety and liveness, right? And you learn about whole families of properties, not just safety properties, just one small part of the set of properties we care about, but we tend to ask safety properties 'cause that's what we know how to prove really well. (clears throat) And when you take, you know, other kinds of formal methods, when you learn like computer aided verification stuff, and you go look at that, then you get a much richer perspective on the world of like truth and correctness and methods and confidence and all these other things.

[1:29:02] So I think, you know, my, you know, I started using proof assistance in 1993. I learned PBS and I learned ACL too. I still hold a flame for ACL too. I still think PBS is beautiful. Most of you people have probably never heard of either of them. You probably don't even know those things existed. And I think, so I've been using proof, I've used proof assistance for a long time, but I think until 2026, I think the payoff was not a great one for me. You know, I've had students who've used, done PhDs using Coq for like crypto protocols, where they're, that is a good use, that was a good use case because the level of confidence we want is high and the size of thing we're working with is small, right? Like that's a nice, so Jay McCarthy's dissertation was done entirely using Coq. So Coq as was called, and Coq now. But, so I think I've made some excursions into that, but not a lot. I think now things may be a bit different, now that maybe agents can generate proofs. I'm optimistic, but also wary.

[1:30:08] I'm optimistic because it looks like, it used to be that we had automation and non-automation. And I was always biased towards automation. And now it looks like the non-automated stuff can be mostly automated. The problem, the thing that worries me is, what happens when the automation doesn't work, right? Because either the thing is not true, in which case the automation is never gonna work, or you know, whatever, your latest model, Gen AI model, whatever is not able to find a proof or something, what's the failure mode? Because there isn't a thing that says this is not true. There isn't a thing that says, you know, it just, you spin for a while. And then like, now what, you're gonna take a user who's never used a proof assistant before and then give them what, like this massive trace and say, this trace was not sufficient for proving this. Well, what is the feedback mode here, right? Like again, if you have a very experienced, you know, rock user or lean user or something like that, you can say, look, I'm gonna try this. I've got, you know, here's my set of tactics. I'm gonna try applying this. And you can look at that and say, oh, that didn't work.

[1:31:10] Let me see what else you'd, let me try to audit what you did, right? But the whole point of like push button automated verification is you don't have to know anything about what's happening underneath, right? When you run a model checker, you just click the damn button. You run SAT solver, you just click the damn button, right? Here, you click the button and you're gonna get a thing called a tactic and it doesn't even work. And like, what is a tactic? What does any of this mean? I will say, I think there's an exciting research question here, which is how can we surface that failure in a way that might make sense to the user, translate it to the user such that they might be able to give tips and say, oh, if that's what you're trying and that happened, then maybe this other thing to try, use their knowledge, their semantic knowledge of the domain to try to aid it, right? I think there's super exciting potential there. There's a huge human factors research problem there, right? But until that human factors research problem has substantial progress, I would never use what's solved. Nothing's ever solved. But unless there's, until I see substantial progress, I'm gonna continue to maintain some of my skepticism because the thing, as I said, is people don't actually don't care about proofs.

[1:32:15] Very, I mean, when I say people, the problem is the people listening to this podcast do. But they're like a tiny sliver of humanity, right? I mean, I don't know, maybe you have like, I don't know, maybe like 1 billion listeners by now. So it's maybe 1/7 of humanity, but there's still 6/7 of humanity left, right? Or maybe you have slightly fewer than 1 billion listeners, I'm not sure. So my point being that there's a sliver of people, and I think, again, this is back to this 10%, 90% thing, we over-index on people like ourselves. We're all like an in-crowd, and we all love proof assistants and proofs, and sitting there and looking at, you know, defining new tactics, and applying tactics, and applying reductions, and using our lovely Emacs keystrokes, and all these other things. And most people don't give a damn, they just wanna know like, is this true? Can I be confident in this? And I think if we could reframe our questions away from proof, which is what a proof assistant for, to truth or even confidence, then we might get a much, we might be able to exploit the much bigger space of like formal methods out there. There's my like, there's the gentle version of my answer.

[1:33:19] (laughing) - Well, thank you so much, thank you. I actually asked this, maybe I should have started with this, but it's, some students started, some people started showing up to me saying things like, I wanna learn more of this, like what should I, where should I go? And I started thinking really hard of like, where should I point them? Because my, the way that I think about programming languages is more the proof assistant side, but what is the point? Like, why would anyone, like how would they use these things? And this is where I'm trying to navigate, like what is the value that I can give to the 90% here? And that's an open question for me as well. - Very open question. - Exactly, but I think I'm a little more optimistic than you are, and I have high hopes for things that we can bring to a bigger public. Moving forward then. I think, look, I don't wanna, I don't wanna deflate anyone's optimism, I would never wanna do that. I think optimism is great, and I think we only make progress by being optimistic.

[1:34:22] The only thing I would say is, what I've learned from many years now of doing human factors research and like, you know, studying cognitive science and so on, is that we don't, if we don't understand how people learn and how people come to like figure things out, all of our good intentions are not worth very much. We have a lot of good intentions. Everyone here is well-intentioned. We want to do well. We wanna grow the community. We wanna do these things, but at the end of the day, you have to understand like, not only the technical, but also the sort of the human, the emotional, the social, the affective, all these other mechanisms. You know, there's like, sociologists, for example, will talk about things like legitimate peripheral participation, how, you know, people, unlike, you know, it's the natural CS thing to think like, everything we don't know nobody's ever thought about before, but of course that's not true, as you both well know, right?

[1:35:25] And so sociologists, for example, have thought a lot about questions like, how do people come into communities and how do they join communities and how do they become members of communities, right? So, for example, there's a notion of what's called legitimate peripheral participation, which is like, people start on the periphery, they find what are considered legitimate activities of periphery, they start performing those activities and then they start moving towards the center, right? So, if you wanna grow a community, you have to think about, if you buy that theory, which is fairly robust, I mean, there's some versions of it, but it's all fairly well studied stuff and other things, like not just, you know, programming languages, but like, how does one become a car mechanic, right? Like, those are also things that are highly technical things that people start on the outside and end up on the inside eventually, right? And so, I think to really succeed, we have to think about what are those mechanisms and how do we create opportunities like legitimate peripheral participation so that people can actually become part of the community, right?

[1:36:27] And good intentions are not a substitute for they're necessary, but not at all sufficient if we don't understand how people learn and how people form communities and how people become parts of communities, our good intentions can end up being like wasted. That's all I'm trying to say. So, the optimism is great, but the optimism should be wedded to like some other kinds of knowledge as well. - Maybe you didn't realize, but I think you actually gave a thumbs up that what I'm doing is actually on the right direction, given the model that you're bringing up, because that's exactly my focus here, is building community and being more welcoming to the outsiders, so great stuff, yeah. - Yeah, I think this podcast is fabulous. I think this podcast is fabulous and that's why I'm delighted to be on it, right? Like I think this, we need more of these kinds of things. I think we need more blogging. I think we need more podcasting. We need more communication. We need to tell the world what we do. And I mean, I looked at the topics you guys do. I'm like, this is fabulous. I think it's absolutely the right kind of thing and the community should have much more of this and this is fabulous.

[1:37:29] I couldn't agree more. I am completely endorsing your claim. Let's move to a JTIC programming finally then and talk. - Before you do, Dan seems to have a comment. - Oh, well, I wanted to have a transition point that will get us into the agent. - There we go. - Because I totally agree with everything that you've said about truth and confidence and proof. - But, but, but, but, but, just get to the but, yeah. - I mean, it would have been, I would have agreed more last year. But what's happened is the agentic stuff has pruned away so much stuff that I used to think was very, very important. Like you talked about the Emacs keystrokes. I haven't opened Emacs in, since I entered industry a few months ago, right? I've just been in Codex, who cares? And so it's also changing a lot, or I hope it is, of the way that we, that students learn and the way that we teach. So the question is like, shouldn't the focus now be more on, especially at Brown?

[1:38:32] Like wouldn't you want Brown students to be the ones who are most producing the most reliable code, the code that you have the most confidence in? And shouldn't we maybe be changing the direction of pedagogy in response to these agents to be teaching more reliable forms of programming, this proof assistance earlier in the curriculum, making that more of the focus? And then maybe that would also just be better for their learning experience. It's harder, stuff that's currently harder to feed to an LLM anyway. - I mean, we've been doing formal methods education at Brown for like 10 years now already. So we've like, I'm glad everyone also slowly catching up. But no, I understand the point you're making. I think it's a more complicated point than that. Yeah, I mean, yeah, so sure. Let's get into the agentic part. I guess this is our segue to get into that. - Well, I mean, my question was, should it be eating into the earlier courses more and more? Like should we spend less time on tabs versus spaces? - Look, look, the most intellectually honest thing that I will say is I don't know.

[1:39:41] And when I say I don't know, what I do not mean is I don't have opinions, okay? The difference is as somebody who's also an education researcher, I approached this from a point of view of like epistemic humility. And what that means is there are things that I know to be true. And there are things that I genuinely do not know about. And I think when it comes to agentic programming, what I know is I have like giant ignorance and giant blind spots. And those are two different things, right? And therefore I'm very cautious about making statements. So the reason I demurred when you said that and I said, sure, maybe is like, I don't know. It may be the case. It may also not be the case. Now, having made that disclaimer, I can now tell you my opinions, but I really wanna be clear that I think we do not have a body of knowledge here. We don't even know what question, we barely know what questions we should be asking. I don't think the computing education community is of any help here in the slightest, unless there's like a small number of people.

[1:40:45] I mean, there's a handful of people, like Ben Shapiro at U-Dub and Mark Gosdale at Michigan, and you know, people like Amanyadov at Michigan State, people like that, handful of people who I've talked to who I think are actually trying to think hard about these questions, but a lot of the community is just like, oh my goodness, it is so sad. So that's maybe the most provocative statement I'm gonna make here. But we just don't know, right? So everyone's got an opinion. I would say like, you know, you know, as the old saying goes, your opinion and like 250 gets you a cup of coffee, except I think even 250 doesn't get you a cup of coffee right now, so, but that's as much as most people's opinions are worth. What I think we need to do is we should approach this the way we do, this has been my thing for years now, right? Is why do I approach my education work with, my caricature of the way education is presented is, you know, imagine if I wrote a, you know, a compiler's paper and I sent it to, I don't know, like PLDI or something like that.

[1:41:55] And it's like, okay, here's my compiler, here's my language, here's my optimization, and you know, here's detailed semantics, evaluation. It's like, well, I don't know, I tried it and it was really awesome. I mean, I asked like a guy who ran the compiler, he thought it was really great too. I also asked the guy in the office next to me and he thought it was great. So there you go, sounds great. You would be humiliated, you wouldn't even think of submitting that as a paper, you'd be like, what am I doing with my life here, right? And yet that is mostly the level of evaluation we do for most of our education. I don't understand why we are so rigorous. You know, you don't even want truth, you want proof, right? When it comes to like a piece of dead code, right? Like inert code, you want proof. When it comes to like your teaching, you know, it's like, ah, man, whatever, man, vibes, whatever, right? Why don't we bring the same rigor to our educational work as we do to our research work? I came to feel like this was like a fundamental mismatch and I could not answer the question. I could not tell myself why it is I had this disconnect and I decided I was gonna stop having this disconnect in my life, right?

[1:43:00] So given that position, I have to be very careful about statements because I don't know, right? Maybe it would be amazing to start all courses, you know, with lean and proof, maybe, I don't know. I think there are gonna be all sorts of negative consequences of doing that as well and I think lots of people should try experiments but I think the experiment should be like actual experiments, not what we mean when we usually say I'm doing an experiment education, which is I'm just gonna do a thing, right? And if it goes well, great, and if it doesn't go well, well, you know, what do you know, right? But actually treat it more like a proper experiment. I mean, I'm not saying like you don't have to go overboard, like, oh, I'm gonna pre-register my hypotheses on preregister.org or something like that, right? It'd be good, you could do that but I think you should at least like approach with at least some of the both humility and honesty with which we approach education or research to doing education and do these experiments. Report back honestly, right? Because otherwise what'll happen is the people who love lean will find that lean works, the people who hate lean will find that lean doesn't work, right?

[1:44:04] The people who love X will find, you know where I'm going with this and we won't actually have learned anything because each person would have done their own like weird completely different thing and there's no attempt to produce generalized knowledge which is not how we operate when we're doing our research. Sorry, that's a very long rant but I think it's important to get that rant out of the way. And then we can talk about our opinions now and ideas. - We're gonna cut out the entire thing when we repost this on TikTok, 60-second clip. (laughing) - Excellent. - But so- - The best kind of censorship, yeah. - Yeah, so what is your kind of approach I guess to the- - You know, so as I think you folks know, we did this course this spring. Basically here was the genesis, right? Is I got clawed-pilled over winter break. I went to my colleague, Kathy Fizzler and I said, you gotta try this out. She was like, oh God, this is none of your crazy things. I'm like, no, no, no, you really, trust me, you really have to try this out. She's like, okay, great. She went and got a subscription and she came back a week later and said, okay, I see it. I get it, what are we gonna do now? And so we both agreed something has to change for the fall but also being, you know, my instinct was I'll just try some random thing.

[1:45:15] And she's like, no, no, can you please not do that? And so, you know, because we teach intro classes, right? So like the entire rest of the department gets affected by what we do. So what she pointed out was like, you know, there's this well-documented phenomenon in education called the educator's blind spot, the expert blind spot. The expert blind spot is simply we are not capable of putting ourselves in the shoes of a novice. We just cannot, no matter how hard we try, we can't, right? And you see this all the time. Like you come up with an exam, you hand it out to students and somebody writes an answer. You're like, what on earth have you written? It's like, well, can you please explain what you were even thinking? They're like, well, I interpret it this way. How on earth could you possibly interpret that question? Well, that's just your expert blind spot. That's all that's happening, right? This is well-documented. We can't be novices. We cannot really put ourselves. So Kathy and I said, well, there's only one way we can do this which is to actually get some real novices to give us their feedback, give us their thoughts, right? So, I mean, the problem was she was on teaching relief and I was on sabbatical.

[1:46:16] We're like, it's too much fun. Let's just do this. So we decided to create this course called the Gentic Studio with Michael Litman. Idea was all coding would be done with like cloud code. Everybody got a $20 subscription. The $20 was intentional. We said, if you give you a hundred dollars, you'll spend day and night on this. You'll fail all your other classes. So we think it's actually healthy for you to take only the $20 and have cloud back you off. And it turned out that was a good idea. So we said, you're gonna do all these programming projects. We're gonna like set up the sequence of assignments and whatnot. We have no idea what we're doing. We're literally assembling the plane mid-flight. That's what you're signing up for. This is not a course. This is essentially a research project. And they're like, yep, we get it. We're guinea pigs, we're good with that. And, but the key thing is for every assignment we want from you a reflection journal. And the reflection journal is what were you expecting? What proved to be easier? What proved to be harder? What didn't go as you expected? Et cetera, et cetera, et cetera. Okay. - And you mentioned about the expert blind spot. So these students, they don't know how to program.

[1:47:20] - Yeah. So these were not students who knew no programming because we were not confident. Sorry, there's gonna be a lot of negatives in the sentence. We were not confident that there would not be a moment, meaning we thought there might be a moment when people actually have to look at the code. We didn't know, right? So the assumption was maybe they need to look at code. And if they've never programmed before, and we're like, go read, I don't know, like JavaScript code, they'd be like, what am I even looking at? This is hieroglyphics, right? So we took students who had minimal but not zero programming experience on purpose for that reason, okay? So also our findings are a little colored by that fact. Like we don't know what a true novice would do. But some of these students are actually a pretty good representation of the end of the first semester, right? So if we start putting agentic stuff in like, you know, two months into the semester, that's not terribly off, okay? So anyway, so we said, okay, you're gonna do this, but the journals are completely written by hand. No AI for the journals. Journals, we wanna know what you think, not what Claude thinks, right? So you write the journals, you turn in the journals, we set up the sequence of assignments with a whole bunch of learning objectives.

[1:48:22] We went through this entire semester. And what we've been doing over the summer is actually analyzing the journals and trying to figure out what we've learned. We're in the process of like, still in the middle of that analysis and got various findings. We've actually been updating the course page. We have a link on the course page to, there's a link that says for visitors because a lot of people have asked us. So we're like, as we keep learning things, we're just gonna keep updating this page. So you can just go to the course page and look for for visitors. You can see what we're learning. But we're in the process of doing that. And now we're starting to rethink the design of our intro classes in the fall based on what we've learned so far. So that's, we're just starting to get into that phase now. So this is just science, right? We don't know, we acknowledge our blind spot, which is a critical part of it. We're gonna set up a machinery by which we can learn. That is the journals and also how students perform and various other things. And now we're distilling that into knowledge, like disseminateable knowledge. And then we're gonna take that knowledge and redesign based on that knowledge. And right now in the midst of that redesign, we're just starting to do that like today, yesterday, something like that.

[1:49:24] - Can you share some of your findings so far? - Okay, here is I think the easiest and highest level one I can say. Until AI, especially agentic programming, educators had really good feedback mechanisms, which is you could give an assignment and if the assignment was too hard for someone to do, they would either come to office hours or they'd post on the forum or they just wouldn't turn in a thing or they'd come and tell you this is too difficult. Or there'd be some machinery by which you could start to get a sense, even just you come to class, right? And you're like, you all seem kind of tired. Yeah, what, oh, the continued fraction assignment? Yeah, like, okay, good. That gives me a sense that like, okay, this is a harder assignment versus this other assignment. They come to class having slept well enough, right? Now, because there is essentially nothing you can do in an early course that Claude cannot do, right? And we're not giving like factorial or anything like that.

[1:50:28] We're giving like serious programs, but they're serious programs from the point of view of a novice, right? But they're not serious programs from the point of view of Claude. Now, of course, as you know, there was some assignments that did turk about Claude. We can talk about that separately. But by and large, you know, you're building reasonable things, you know, you're doing like data analytics or you're building like a sports tournament site or you're building like a, one of the assignments was like, you know, a checking for like, you know, graduation requirements, things like that. So the thing is, well, one was like a chat bot kind of thing, right, Claude will produce code like Claude or whatever agent you wanna use. It'll produce code, it'll produce a nice user interface. You might have no clue what it did, right? But the point is you can still produce a thing in relatively small amounts of time that meets all the expectations, is actually quite sophisticated and you have zero knowledge of what happened. And what that means is all of our previous channels for feedback no longer work. We are going to have to figure out new channels by which we can get feedback about what is actually happening to the assignments we hand out, right, how are the students faring?

[1:51:31] When are the students overwhelmed? When are the students completely lost? We had several students who worked on this chat bot that like, so we use a thing called matrix, which is like a open source, like a server thing. It basically think like WhatsApp or Discord, you know, they all have like Discord, right? There's this sort of look and feel, like Slack and Discord, there's channels, there's like servers, there's channels and each channel, there's like a thread of messages. So it provides like a server infrastructure for that, right? So we're like, you're gonna build clients for that. We did like a testing part of it and then you're gonna build clients, we're gonna host the server, you're gonna build clients. Okay, so you build clients and turns out many of them didn't really understand what it was. So I had said, look, I'm gonna give you a brief introduction to like what's happening with Discord and what, you know, not with Discord, with like matrix and you know, roughly what client server is, but you've also got access to a cloud subscription, feel free to ask it questions, right? And everyone, you know, if you believe Twitter, everyone in the world is gonna be learning like this, right? But what if you don't know what questions to ask? Now, I had actually checked, right?

[1:52:34] I had gone through like, you know, I'd spent like two hours, three hours with Claude checking that it understood matrix well enough that it wasn't like, you know, hallucinating answers and whatnot, it's got a pretty good knowledge base about matrix, it's pretty robust, right? Okay, but that's because me with 40 years of expertise knows what questions to ask. These students, many of them had no idea what to even ask. What do I ask to learn it, to learn from it? No idea. So like, what's a client server architecture? It'll give you like three paragraphs of what's a client server architecture, but if you don't, even if you know to ask the question, you may not have any clue what the answer is. You could say like, explain that word, explain that word. But I mean, just imagine like, think about a language you don't know, right? And yeah, you can have a dictionary and you could look up each word. After the seventh word, you've lost track of where you are, like what is even going on, right? That's the kind of experience they were having. So A, this like, oh, just ask Claude. It knows the stuff is not actually good because they don't even know what to ask and they don't know how to make sense out of the answer. But also for us, like the loss of channels by which we could discover how our students were doing.

[1:53:37] Because again, the tendency is I've got a cloud subscription instead of posting the forum, I'll ask Claude, right? So we had given them and told them to use it. And that was the thing that was robbing us of the signal that we desperately needed. So those are the kinds of experiences we were having that, you know, I'm sure some people will be like, oh, that's obvious. I think to me, fairly obvious in retrospect, but certainly, well, I wasn't smart enough to figure them out upfront. - So you've mentioned that you already have some data in which you can change the courses in the fall. What kind of changes are you thinking about? - We don't, you know, it's too early for me to tell, way too early for me to tell. I don't know. We are literally in the midst of doing that and I don't wanna speculate because I don't know. I genuinely do not know. And partly also-- - I was gonna ask, how does it make you feel? Because it's such a major turn point in how education works. - Oh, it's fabulous, man. It's great. In 2010 or so, I had a paper at SIGCHI, which is a human computer interaction conference, right?

[1:54:42] And I went, I was like, oh, I'm curious to see what SIGCHI is like. So I'm gonna go to SIGCHI. And I went to SIGCHI. And I walked in and I realized, I don't know anybody here. Nobody, right? I am like, you know, like, you know, when I go to a PL conference, you know, some of the students know who I am and they come and talk to me and it's great, right? I don't know any of these people. And I remember thinking, there was this moment, I remember thinking, even as much as like there's a notion of status, I am like a lower status than even some of the graduate students here. Because like the grad students from the big groups, right, they're there with their advisors and our fellow lab mates and everything else. And I am like lower than even that, right? And I was like, I thought about it for a moment. I was like, how does this make me feel? And I thought, this makes me feel so alive. It makes me feel like being a grad student all over again, right? It was like that excitement of like ignorance, but the potential, the entire world was in front of me. And like the potential, the ability to discover and knowing that here's the thing that I had that those grad students didn't have, right?

[1:55:52] I had been down this road before. I had the confidence that I can learn a new thing. I had learned a new thing before. I had been there and I'd gotten out of that and I could get out of that again. And I knew I had the confidence I could learn. I've learned, I've taught myself education. I've taught myself security. I've taught myself enough cognitive science to like vaguely sound knowledgeable. So, so what? It's like a new thing, we'll learn. That's what we're paid to do, right? Like there's no point covering in fear. That's the only choice. - Does it make you at least the least afraid that students are not gonna learn how to actually program anymore? - So I, you know, I think there are thought experiments and there's certainly, there is a thought experiment you could work through, which is what if nobody ever writes a line of code again? I mean, maybe somebody will, maybe I don't know, maybe the, actually not even people at whatever, anthropic seem to write code anymore. Maybe, maybe we'll never write a line of code anymore, right? - Maybe, maybe C.O.B's obfuscation competition is gonna be the last kind of handwritten code, right?

[1:56:57] (laughs) - Is the only, yeah, you're right, you're right. That'll be the last place where any human being will write code and maybe even not even there. I don't know, right? So, okay. So what? Sounds like progress in some ways. I mean, the danger of course is we're gonna get like a whole bunch of terrible systems, right? I think we are. I think we're about to see some really crappy systems out there because people like vibe coded it and like put it on Bursale or whatever and like that and we're gonna have to deal with the consequences of that, right? So I think that is a real danger. But, you know, I mean, I'm very conscious of the fact that I wanna end up not being somebody who's like, I really want this to matter because I spent 40 years getting to be good at it, right? Because that's when you become regressive, right? That's when you're like, you become anti-progress because like, I don't wanna admit it, but really the thing is like, otherwise like I spent 40 years on nothing, like what was the point? I mean, I don't think I spent on nothing. I think I learned things along the way. But I don't know.

[1:58:00] I don't think that's a healthy attitude. I mean, I think it's also not healthy to go to the other extreme and be like, oh, nobody's ever gonna code ever again. So we don't ever need to. I think the interesting educational challenge of the moment is figuring out what do we do? What is the right learning progression or what is a good, I shouldn't say the right, what is a good learning progression? A lot of it will depend on the individual students, the institution, the institutional needs, et cetera, et cetera. Because again, we're like, we live in a society and et cetera, right? But I think there's an exciting question here, an open, very open research question, right? Part of the point of the agentic studio code was, as an experiment, what if we never had anyone write any code by hand? And it worked pretty well, right? It had some downsides and that's what we're trying to explore and understand and figure out how to fix. But I think a computer science department needs to ask itself, why does it exist? What does it provide? What does our value add to the world, right? Until now, our value add was always like, well, we're the only people, we're the only high priests who know the hieroglyphics.

[1:59:08] I mean, I'm referring to Python, of course, but we're the high priests who know the hieroglyphics and nobody else does, so you gotta pay us a lot of money to give you hieroglyphics. Well, now it turns out there's like a hieroglyph generator, right, and it generates it faster than you can possibly read it, okay? So what is left? What is left is quality, right? We have to be the people who are the bastions of quality. Now, this is where proof and truth and confidence and all these things come in, right? Like that is still the thing that I hope that computer science will be the subject that teaches people how to produce products that we can stand behind, because the vibe coders will not know how to do that. That's at least an assumption, right? There's a wonderful talk by David Lord Parnas from 1998. He gave a keynote at one of the software engineering conferences and he said, you know, a very provocative title, like very Parnas, it said, "Software Engineering Colon, An Unconsummated Marriage," right? And what he was basically saying was like, there's engineering, which is a set of disciplines with a set of like, you know, expectations of professionalism and so on.

[2:00:10] And then there's software, which is like calls itself software engineering, but doesn't do any of the things that engineering does, right? Like, you know, one of the things he points out is like, engineering products come with warranties. Software comes with disclaimers, right? You go to the store, I mean, in most countries, you go to the store, even like a $1, I don't know, like a 100AS, whatever, like a plastic product, right? Will come with a warranty and if it breaks, you can go back and say, look at this stupid thing, I paid a dollar and it broke and be like, we're sorry, we'll take it back and give you a new $1 piece, right? You can pay a million bucks for a piece of software and it breaks, I'm like, look at the end user license agreement, did you not click accept? You said you accepted all the things that happened with it, right? So, maybe finally, we're gonna be forced to be like, our value add is not just that we're like, you know, we're pyroglyphics producers, our value add is we are the people who teach students, get our students to learn how to stand behind products, how to be able to like say, this product actually has some, you can have expectations, I can give you quality, I can deliver quality.

[2:01:21] And yeah, that's scary as heck, but it's also exciting, right, like this is the dream of formal methods, finally, we're the only thing that matters. Hey, yeah, but you know, I talked to like intro programming people and they're like all, like they're finally, their stupid factorials have been destroyed, right? Like it's too trivial and they're like, oh man, like what do we do? And everything, but it's funny because you talk to like people who teach CS1 courses, they're like, I don't teach programming, I teach problem solving. Like they love to use this phrase, I'm like, well, okay, so now the programming part's trivial, why don't you teach the problem solving? That's all that's left, you should be delighted. Well, they never taught problem solving, they just taught programming, right? As my colleague Emmanuel Schranzer likes to say, you can't claim to teach problem solving just because you give a lot of problems to solve. And that's what they've been doing, we're just gonna give you lots of programming problems and if you solve them, I guess we've taught you problem solving, well, now that's no longer the case. So now you should be delighted, right? Like all that's left is the part that you claimed you were teaching, so do it.

[2:02:23] Why are you, what are you afraid of? I think they are afraid because I don't think that's really what they did. So I think it's exciting, I think it's super exciting, it's scary as hell, of course, but yeah, it's just another challenge. I mean, you know, we've been working on this op-ed that hopefully will appear in CACM at some point and you know, Grace Hopper, right? Like think about, you know, she wrote her first compiler and in like the '50s, right, she wrote the first compiler, like it was maybe as an assembler compiler and people told her for two years, I found this quote in the Computer History Museum where she said, people said, "This can't work." She like, "I've got a working program." They're like, "No, no, no, it can't exist." They told her, "Computers can only do arithmetic, they can only do numbers, they can't do programs." And of course, now the irony is like, LLMs can only do programs, they can't do arithmetic, but anyway, so they told her like, "It can't exist." She's like, "It's there, I can show it to you." Like, "No, no, no, it can't possibly exist, computers can't do that," right? And, but you know, eventually we all lived in our world and you know, the next thing she did was she worked on a language called Phnomatic, which because it was the predecessor of COBOL, where she was like, "Let's try to make programming languages as close to natural language as possible." And for decades, the PL community laughed at her.

[2:03:38] It's like, "No, you naive fool, of course programming languages are not like natural languages. We are like precision, we are semantics, like that, blah, blah, blah." Guess what, we're all programming it now. Like Grace Hopper, "I wish she were alive for this moment, man. I wish she were here because she could finally say, yeah, that's what I've been trying to tell you, muckers." You know, like, I don't know what words she would have used, but I hope she'd said that too. She would have finally been like, "Yes, 60 years later, I'm finally right." But that's what she was dreaming of in like 1956 and 1958. We can do it now. What do we, how do we empower ourselves? That's the question we should ask. And I think what we have to accept is, empower ourselves while teaching students how to take responsibility for products. That is gonna be our distinguishing characteristic. And the BIPE coders, by definition, are the people who won't, don't, can't, whatever, right? They're like, "I'm gonna generate, I'm gonna get taught to generate tests." Well, that's also known as a correlated failure.

[2:04:41] For trivial things, that'll be fine, but trivial things, nobody's gonna get paid to program anymore. But for complicated things, that's not gonna work so well because of correlated failure. And if we teach students what correlated failure means and how we avoid it and how to write not just unit tests, but properties and how to elicit properties and how to turn properties into maybe things that you send off to model checkers or model finders or proof assistants or whatever, and show how to like produce software that you can stand behind. But what a world that would be. That would be amazing, right? Just imagine. - I'm pretty tired, but let's, let's, I really wanna, I really wanna rehash this debate. (laughing) I'm baiting Dan, man. Like I am so baiting Dan here, yeah. - I don't know, actually. I actually don't have the energy for the debate. What do you think, Shreeram? I mean, we had this discussion on Twitter where you posted a piece of writing. It was for an opinion piece. I don't know the context of it.

[2:05:44] And you're saying that this is beautiful. I wish that I could write like this so that all computer scientists, you didn't say that all computer scientists would write like this. You didn't even-- - And it was very flowery and you didn't like it at all. - Yeah, and I mean, I, there's so many different ways to come at it, but I guess my question for you is like, what do you think is the difference between good literary writing and good technical writing? - Yeah, I think that's a great question. As somebody said, as somebody who studied humanities, it was kind of weird for me because when I was studying humanities, I was like, oh, this is completely different. I'm like, this is my STEM brain. This is my humanities brain. And these are two different things. And then after a while, I started to realize, you know what, there is actually, they're more similar than I thought. Like they both have a kind of rigor to them. First of all, it's not like, oh, STEM is rigorous and humanities is just like, you know, vibes, right? Like, I mean, that's like the average person on the streets opinion about like, oh, you can just write anything you want. Like in my opinion, and you know, and actually that's not how it works, right?

[2:06:48] In fact, I think my most formative thing was I had professors who called out my bullshit. I tried like BSing my way through one of my first humanities courses. And I had this amazing professor who just like completely called me like, I don't think that's at all what the author's saying. I'm like, oh. And I'm like, oh, I'm gonna have to actually read and understand what's going on. And I was like, it was like refreshing that somebody was willing to, you know, will like take me to task in front of a class. I was like, yeah, I'm gonna, this guy's gonna teach me stuff. And he did, he taught me so much, Conrad Kent. So I start to say, ah, there's actually deep rigor and they actually have some similarities of method too, which is they're all like, you know, they're trying to understand things. They're trying to get to the bottom of things. They're trying to get to the essence of things. They're trying to uncover layers, et cetera, et cetera. You know, just the way we peel away abstractions to computer science. In humanities also, you try to go below the surface, you know, go past the text and you go to the subtext. I happened to study humanities when post-modernism was like all the vogue. Some of which in retrospect looks extremely silly and even then look kind of silly. But I actually think it was also deeply valuable because I think it was very interesting to ask questions like what is the text behind the text?

[2:07:52] What is this thing actually trying to say, right? I was doing the same kind of metacognition there that I was doing in like, you know, metacircular interpreters. I mean, it's not exactly the same, but like you were going behind the scenes and looking at the thing that produced the thing and asking questions about the thing that produced the thing. And so it was like, I actually see some, there's, you know, there's a certain connection here, right? But I still thought like writing was completely different. So when I wrote humanities stuff, I wrote in a sort of very whimsical style and, you know, STEM, you know, I didn't, I certainly did, right? And I had an advisor who's an amazing writer who taught me how to write. Like I got to grad school and I thought like, I know how to write, man. Like I've done writing across all kinds of disciplines. And it took like two to three years before he finally convinced me I did not know how to write and like sort of rip my writing apart and rebuild me from scratch. But what I also learned is like his style and my style are not the same style at all, right? And over time I learned my own style. And now when I teach my students how to write, I'm like, look, we are not necessarily going to have the same styles. My job is to like teach you how to write in, I'm going to teach you how to write in my style.

[2:08:55] It's a thing that works, but when you go out, as you get older, you will discover your own voice. And when you go out, you will write in your voice. And I encourage you to do that, right? But while we're together, you're going to learn at least one style and that's probably going to be mine. All right, so my style I think is more literary. I do care a lot about the words that I use. I routinely get docked by program committee members, you know, like I have to say there's one thing I will never do, which is when a reviewer asks like, this word, I don't, what does this word mean? I'm like, it's 2026, you can double click and open a dictionary, you know, like it's not that hard. And I don't think it's actually, like if you, like sometimes if you gratuitously use big words, that's a bad thing because you're making your paper less accessible, but sometimes when you find exactly the right word to capture a sentiment, you want to use that word, it's there for a reason, it exists in the language for a reason. It's not like you're not trying to be obscurant, you're trying to like actually get precise. It's like as semantics, we should value that, being able to say exactly what you mean and not like something vaguely around what you mean, right?

[2:09:59] So I think, so that's one part of it, that's a choice of vocabulary. But I do think we try to write too scientifically, that's in double quotes, scare quotes, and that is a kind of stiffness and formality that is more about impressing each other than about actually communicating with each other. And at some point I got the confidence to say, I don't need to do that. And it was very liberating. And what I found is that it doesn't actually hurt me, right? Now, if it hurt me, then I'd have to actually make a compromise here. It's like I have to decide which way do I want to lean on this? But it turns out people actually enjoy reading a well-written paper. I view it as kind of a dishonor if I submit a paper and at least one reviewer doesn't say this was a well-written paper. I'm like, oh man, I completely screwed up. I don't care about the decision. Like I want at least one reviewer to say this was really well-written because like that's the effort I'm putting in, right? And so I'm not gonna say my style is literary, but I think it's more literary than many people use, but it's also more bottom up.

[2:11:07] It's more example-driven. It's more like, I always like to start with like a worked example. This is my pedagogic style coming in, right? I start with the concrete before going to the abstract. When I have a tool and it has a semantics, the semantics comes later. I always go through a workflow of the tool so you can see what it would be like to use this thing, to run this thing. I spent a lot of time finding that one right example that's gonna illustrate the key features that I wanna illustrate and show you that. And then I'll say, okay, but behind the scenes, what actually happened, right? And I think this is, I wouldn't say it's necessarily literary, but it's a bottom up style. It's a more pedagogic style. Like my goal of writing the paper is to teach somebody something. And if they're not impressed at the end of the day, like, oh well, but it turns out, I think people don't mind that at all. It, I mean, it's, but that's, you're just saying what I would say normally. And I mean, because, let me read you something that I have, you've written in another tab. You wrote, people often ask me for recommendations on pedagogy, period.

[2:12:15] Very short sentence, all very simple words. To avoid repeating myself, I'm gonna make some suggestions here and update this document over time. The rest of the blog posts, it's written in this very, very short sentences, very accessible words. Maybe you'll throw in like a very precise word somewhere in here, but I think as a rule, the way that you write is very different from the way that you highlighted in that particular Twitter post. - Oh yeah, yeah, yeah. In that sense, yes, yes. I was very influenced also by modernism. I remember reading like Sartre's "La Trangé" and it was like, it was like just like slamming the face like a ton of bricks. Like that first sentence of that novel, like just destroyed my like notion of literature. So, and you know, my advisor was a huge Hemingway, totally a Hemingway person. You know, he gave me, Hemingway is a, what's the Paris book? What's the Paris book? - A movable feast? - Yeah, movable feast. He gave me a movable feast. He was like, this is great writing. And I read, I'm like, yeah, you're right. That's pretty damn good, right? So I think maybe my style is closer to that.

[2:13:17] I think the point was less that it was flowery is more about that like beautiful anecdote. I'm trying to remember the piece and we could find it. But I think it was like the illustrative anecdote, right? It's that memorable illustrative anecdote that sticks in your brain. It was less about the choice of words. It was more about like the, it gives you an emotion. It's kind of like what, what "La Trangé" does, right? It sticks you like, you know, sentence one and like, you know, the narrative's mother is dead. Like that's the first sentence. "Maman died this morning." You're like, what? What way is this? You're, you're stuck. You're like hooked and you are never gonna leave that novel from that point on, right? And he puts you, he plummets you into a situation on, he doesn't start by saying, I am 63 years old. My name is so-and-so. I live in the city of such and such. I have two parents. Actually, one of them has passed away, but the other one was alive. But then, you know, she died this morning and be like, oh, that's too bad. But you know, his whole point was the deracination, right? He just plunges you into the moment. You're like, oh my goodness, what is going on? And the piece that I highlighted had that feel to it. It was like, it was compelling prose that plunged you in and made you think like, I want to read more of where this is going, right?

[2:14:28] That novelistic style is the thing that I thought was so great that we don't do as a community, we don't do. And lawyers do this by the way. Lawyers love to show off how good they are at writing. It's like fun, like law pieces are great. You should always read the, read the first page and skip the rest because the first page is showing off how good they are at writing. And the rest of it is, it's, yeah, it's great fun, but it's great fun. But you know, the point is they will probably look at our papers and say, well, this is weird. But just as we look at like, you know, papers that appear in science, right? Like there, you don't get any literary freedom at all, right? You have a structured abstract, right? Structured paper, it's all optimized to like, you need to as efficiently as possible find the place that answers your question, right? Or, you know, the PL style of like, you know, we conducted an investigation, but you know, the end, we asked the following questions, but the answer is going to be somewhere on page 17 or something like that. But we won't tell you the answer upfront because that would spoil the suspense. We pull the shit, we totally do the shit, right? You try writing like that for like a science, like, you know, like a more traditional physical science.

[2:15:32] I'd be like, what are you doing? What do you think this is a damn novel? Just tell us upfront what your findings are. In the abstract, you tell us your findings. In the abstract, not even page one, abstract, tell us your findings, done, right? And I've tried to, I've realized I used to do that. I've stopped being so coy. So I try to now put more of my findings in the abstract because of like, what am I trying to do here? So the point is like every one of our communities has built up some particular style and all the other styles look completely bizarre to us. You know, it's blub, right? We've got it nailed. These science people have no poetry in their souls. These lawyers are just showing off how well they write. But we've got it figured out, right? And we're all have our like blubs up and down. And so I think it's good to read some of these other pieces because you come away thinking like, oh, that's an interesting thing. Like, I wish I could write like that. Like, I mean, I wish in multiple ways. I wish I had the literary power to do that. But also I wish maybe my papers could start like that. Wouldn't that be a fun paper to write someday? There's two wishes in there. - So what were some of the things that you had to unlearn?

[2:16:37] You said that your advisor taught you that you didn't really know how to write, even though you'd written considerably for humanities. - Oh, I was so flowery, man. So flowery. He was like, just get to the damn point. I mean, this was not just being a humanities student, but also like where some of this writing, especially in like the late '80s, like the early '90s, this sort of Pomo period was like these literary flourishes were all appreciated and like, you know, given credence. - Yeah, why are they like that? I can't read a single Pomo piece. Like, it's just makes no sense to me. - It's a thing, it's a thing, it's a thing. It was a time. So it was an interesting time to be alive, right? So there's that part of it, but also like my upbringing, like I went to, you know, I was trained to write in India and Indian writing is like super flowery. I still, I tell my kid, you know, I had this English teacher, I'll never forget. I'm not gonna name him because I don't know. But he literally, he said, listen, when you write, you should write well. I'm gonna give you an example. You don't want to say he came, what was it he said?

[2:17:44] You don't want to say he came first. You want to say he came second to none or something like that. I'm forgetting the exact phrase now, my kid would remember. You know, things like that. One word would suffice. You have to use like this big flowery phrase that somebody has to like read twice and parse to figure out. Oh, you just meant to say he came first. Like, why didn't you just say that, right? Because that is good writing, right? That was a cultural thing. That was India in the 70s and 80s. You know, the tradition and British history, literary tradition that we had invented and made our own and like distorted in all sorts of bizarre ways. That's what I was told was good writing, right? And I was taught to write that way. And that then got accelerated and promoted and blown up in various ways. So by the time I came to grad school, my advisor was saying, you don't know how to write anything scientific at all. Like, in fact, you don't even know how to write as far as he was concerned. Like, his idea of writing was Hemingway. His idea was drunken white and Hemingway. And like me with my long sentences and like current articles and everything's like, what are you doing? Cut out all of this shit, right? - It just described the exact same experience that I had because Portuguese is so flowery. It's exactly what you were describing.

[2:18:47] And it's really hard for you to get used to this other way, yeah. - Yeah, yeah. And you have these language. So that's the other thing, right? You have the country's tradition, your native languages traditions and all these things tend to like verbosity. And then you get this person who's like, no, that is one word too many. Cut out every single word you don't need. And Dan Friedman's the same way. - Not only learning to write well in English, English is a lot more objective and compact, but also academically, which is so much more objective than compact. - That's right. But the thing is I've drifted away from that, right? I don't write like that anymore. So Mathias writes that way. In fact, when he and I write stuff together, it's pretty fun now because I think we each respect that the other person brings some writing to the table, but it's not ours. And so, you know, it's like an alternating sequence, right? He'll start here and I'll move it here and then he'll move it here and I'll move it here. And eventually we sort of converge like something vaguely reasonable, right? That we both realize like, yeah, each person has contributed something and this is okay. You know? Yeah. So it's not the other thing.

[2:19:48] It's also like super instructive to write with other people, right? Or even, you know, like when I work with my students to teach them writing, like I, we, so what I don't do is I, you know, I don't give them a page marked up, right? Because they're not gonna learn from that. They're just gonna be overwhelmed. What I do instead is I say, we're gonna sit down side by side, you know, shared monitor, zoom, or physically side by side. And we're gonna spend an hour on one paragraph. And we're gonna go word by word. And we're gonna take the first sentence and everything, every single time, what I'm gonna say is, what do you think I'm gonna say about this? Because what I'm trying to do is I'm trying to build them a model, a mental model, right? I'm trying to build a classifier in their minds, right? So they're gonna make a prediction. And this is also, I'm using things that I know from education research, right? They're gonna make a prediction. And I'm like, okay, are you sure? Like, what do you think I'm gonna say? And I say that and I'm like, okay, actually sometimes yes and often no, no. And then it'll be like, Nick, I was actually more concerned about why you put the comma there.

[2:20:51] They're like, wait, what's wrong with the comma? I'm like, well, you see, because you put the comma there, you've implied this thing, but in fact, that's not the same, oh, okay. So now we're gonna delete the comma. Now tell me what you think I'm gonna say about sentence. This is why it takes an hour to do a paragraph. But you do this a few times and they build a, you know, they're all sharp kids. They're gonna build a pretty quick classifier about how to think about writing. And then they're gonna execute that at scale. And that takes a few iterations, a few papers, and then they figure out how to write. At least they write in a certain style until they go discover their voice, just like I discovered my voice, which is neither my Indian or humanities voice nor my advisor's voice. But I do, you know, I do occasionally, I've put in references to TS Eliot's work in my research papers. And I believe, I think it is good for our papers to have some degree of whimsy. And I think we should not be completely unwhimsical. Then it's like just no fun. So I think I would like, if I had to write like one of those pure science papers, which I have, my first paper, but a little too lacking in whimsy.

[2:21:55] I think we should have some fun in what we do. - I think it's funny. I was really surprised how you mentioned Les Congees so well, because that's literally the book I'm reading right now. It's right over there. - Oh, brilliant. Are you enjoying it? - Oh, yes, a lot. I'm still trying to figure out whether I really like it or it's just really weird. Like he, I'm literally in the middle of the book. So let's stop there. - It's a bit of a strange book, that's for sure. It's strange, but it's like that only just like, no. - I wish I could read, I wish my French was good enough. So I could read in French because I'm sure that that's a masterpiece in French. - There's different English translations actually, and they have- - I'm reading in Portuguese actually. I think it's a little closer than French. - Okay, yeah, that's actually, that might be a decent translation there. What depends if Portuguese is more flowery. Well, if Portuguese is more flowery, that might lose some of the essence of Les Congees. - I don't know. But anyways, the question I was gonna ask is, what is about all of this discussion we're having in the realm of LLMs now?

[2:23:00] Does that throw everything in the garbage? Do we still need to write that well? Or is this the same arguments that we're having as learning how to program? What is going on here? - Yeah, I think that's a good question. So, okay, I'll be honest, I've done experiments. This is strictly just for my entertainment, where I've asked Claude or something to write something in my style. And there's enough of my training data on the internet that it gets to about, I would say like 60 to 70% of me. But only 60 to 70%, like there's a lot. I'm like, no, I wouldn't have written that. I wouldn't have written that. Nope, nope, nope, nope, nope. Like most sentences, I have to clean something up. So, to be fair, have you gone back and read your work from 10 years ago and been like, oh, who is this person? It's like- - Oh, it's so embarrassing. So embarrassing. (laughing) So maybe you're not training or all in well enough. - Yeah, yeah, yeah. That's my problem. My talks, oh my God, they're so bad. Yeah, no, it's just so embarrassing. I'll send my wife a text and then I will look at her phone and see the order of the bubbles has reversed.

[2:24:10] And I'll be like, who is the psychopath who texted? (laughing) - Right, that seems so obvious when you sent it. And then when you see it on the other side, like, whoa, yeah. But I think I, so here's the thing, right? I think it's the phrase you folks use. I think writing is very much a form of thinking. And I think where, you know, I saw a message, somebody said recently, right? Like, we all naturally got exercise, right? Just being working out in fields, you know, filling farms, whatever, like, you know. If you look at like farmer's meals, right, there's like a caloric load that would be insane for somebody to have now, right? And yet that's because they were burning it off just by being out all day, like, you know, pushing animals around and pushing bales of hay around and things like that, right? And we stopped that, we had to start going to gyms to like make up for the fact that we stopped doing the things that we just did naturally, walking up and down mountains and, you know, living out in nature and things like that, right?

[2:25:15] And so what is the moral equivalent of that, right? And I think writing is a foundational form of thinking. Now, speaking is too, but my experience has always been that we can be much looser in speech than we can in writing. There's something about the written word that gives us a feedback that says like, it's kind of harder to bullshit. I mean, I don't know, maybe LinkedIn is the counter example, but it does feel like it's harder to completely bullshit in words than it is in speech. And speech also, like, if I'm just talking to myself, I mean, that's weird, but if I'm talking to you, I mean, think about all the cues we're using. I'm using my hands, I'm using my eyes, and we're looking at each other, we're nodding. Moment you nod, I'm like, oh, he already mostly understands what I'm saying, so I can move on to the next thing, right? All this multimodal communication and writing, none of that is there. So I have to get it all there on paper, right? And I think that's why writing is such a beautiful way, like forcing you to think hard, right? Now, of course, there are a lot of people who are like undisciplined thinkers, and they write poorly, right? So it's not like writing is not automatically solving that problem, but it certainly is a very good mode for thinking.

[2:26:23] And so, now, do, you know, if I had to write a whole curriculum, would I use Claude to generate some of the text? I don't know, I'm not gonna be, I think it would be completely disingenuous for me to say, like, oh, I would never do that, right? I love writing, I really enjoy writing, I get a thrill out of the difficulty of, it's difficult for me to write a sentence, and it takes me forever, I have horrible writer's block, and when I finally, like, things gestate, and gestate, and gestate in my head, like I keep riding my bike, and I keep thinking, and I can't figure out how to start, and then when I start, I just write, and it just gets written one time, most of my things I write only once. So that's my writing process, so it's a huge struggle, but when it, it's because it's taking just a very long time to formulate in my head. And once it's formulated, it just kinda spills out, usually just before a deadline. And this is infuriating to my co-authors, who just cannot believe that anyone can be this badly organized in their lives, but somehow, you know, it seems to work for me.

[2:27:26] So for me, like, I would never want to give up writing as a means of thinking, even if, you know, maybe, you know, like, if I had to create the next generation of the Bootstrap curriculum, and I had to revise something, I might go to Claude, and then, but I'm gonna review every diff down to the character, obviously. But I might say, Claude, hey, please upgrade this thing, or, you know, I've put this new data set in, please take this piece of writing that I've done on this data set and repeat it for this other data set, and then, you know, of course, check out the code and stuff like that. But instead of sitting there clacking away at my keyboard and doing all the formatting characters and stuff, having it do that, I don't feel like huge moral qualms about doing that, right? But if I need to think about something, so, for example, one of the questions I asked myself in the spring was, if more and more, most code, that thought experiment of all code is gonna be generated by, you know, agentic AI, then why do we need programming languages, which is a question you guys sort of asked, right? So, I post on social media to see if anyone has a good answer, and nobody gave me a good answer, so I said, I'm just gonna think about this, and I spent weeks thinking about it, and I said, I'm gonna limit myself to, like, a six-page document, because, you know, it's kind of an Amazon six-page memo kind of thing, right?

[2:28:36] Nobody's gonna read more than six pages, and I think I'll need six pages, and so I worked very hard to limit it to six pages, but I wrote up a memo that I posted on the internet, and I was like, here's a memo, here's what I'm thinking, and if anyone has comments, let me know, right? So, that thinking, literally every single character in there was typed by me, right? I cannot imagine substituting even a character of that thinking with an LLM. Like, that has gotta be me struggling to figure out the answers to that question, right? And I think we have to keep that kind of discipline in place, and if you have that kind of discipline in place, then there is, I mean, look, I've written several books, right, I mean, I've written hundreds of pages of textbook. I can tell you there's a lot of routine stuff in there, right, it's not boilerplate in the same census code, but it's kind of boilerplate-ish a little bit, right? Like, once you've spent a lot of time thinking about the right example, you set up the right example, and then everything that follows from that is, it's like, we know what to say, I know what to say, I'm like, oh God, I have to say it, and oh, I have to remember, and for me, it's, like, painful, because, like, as I'm writing it, another thing will come up, and another thing will come up, and I have to make a to-do list, and then, like, GitHub issues, and this and that, and whatnot, and I, it's just this painful, like, administrative thing, where nothing interesting happened, because, yes, if I hadn't thought about it before, while I'm thinking about it, new ideas come up, but if I already know what to do, it's so administratively boring, right?

[2:29:59] So, I'm not gonna pretend that I would never use an LLM to write, I think that would be dishonest, I haven't, I have never published anything that, LLM, I haven't published even a paragraph that an LLM wrote, even a sentence that an LLM wrote, to be clear, I've never published anything, and I can't imagine doing it right now, I might someday, you know, if it's something sufficiently formulaic, I, you know, we wrote this op-ed, every single word was handcrafted, I like writing prose, maybe that's the difference, I hate programming these days, it's like 20,000 libraries you have to import, and, like, do all kinds of, like, refraf stuff, and that's boring, and contrast, like, writing is fun, it's hard, programming is not hard, it's just tedious, and writing is not tedious, it's hard, and I wanna do hard things, not tedious things. - One thing that I learned reading more philosophy papers in this time off that I have, that I had, is that it's exactly what the point that you're making, which is using writing as a tool to think, right? So, in philosophy, it's very common for you to have a lot of essays, which, they're beautiful, they're beautiful, because you can see the philosopher struggling with one single question, and trying to be extremely precise about what's going on, and I think there's a lot we can learn as a community, I think maybe all of the knowledge, all academia can learn about these kind of essays, and discussions, and writing, right?

[2:31:25] - I think we're just gonna value that more now, right? Like, if it becomes the case that, like, building an implementation, writing a compiler, proving it soundness, lean theorem, blah, blah, blah, the usual stuff that goes into, like, I don't know, PLDF paper, if half of that can be automated, well, what's left? (laughs) You know, it's writing the interesting parts. - But it's, I think you hit the nail on the head when you ask about thinking, right? Like, because that's the, I think that's the commodity that we're dealing with right now. It's how much do you actually have to think, and how much of it is actually from a lake? So, that's the turn point of what we're doing here now. - It's back to the expressiveness paper, right? The rest is macros. - Right, exactly. - We just have amazing macros now. If you think of, like, LLMs as macros, if you can do this scaffolding at high-level thinking, the rest is macros. You can say, like, turn this into pros in the style of, you know, so-and-so, and, you know, generate, like, halfway decent pros and whatnot, but that's, like, a kind of macro.

[2:32:27] But, like, the essence of the thing, that's not gonna come out of the LLM. That's gonna come out of my head. All right, I mean, it's, in some sense, like, how we should be, we should get ourselves to the position where we have something interesting to say. - Yeah. - Like, I, sometimes I read, like, you know, these, like, various statements that come out of, like, universities or companies and whatnot, and I, like, for years now, I've been asking the question, say, anything here that an LLM would not have said? Because if an LLM, like, you're basically, if your text looks like the statistical average of what would be said for this, then you could have just said, you know, here's the placeholder, here's the prompt, right? And then, like, we don't even need to burn, like, carbon dioxide, like, we don't need to pollute the planet just to, like, generate the output. You could just give me the prompt and be done with it, right? 'Cause clearly there's nothing original. You're just giving me the statistical mean, right? So the question is always, like, what is the thing that's not in the statistical mean? That's what's interesting. So, like, you should take whatever idea you have, you should ask the LLM to generate three paragraphs about it, and then you should write down your ideas, like as bullet points, ask the LLM to generate three paragraphs, and then figure out which of your points are not in there, because those are the only ones that are interesting and left-worth saying.

[2:33:37] - And I think that's not only for writing, either. That's, like, for everything, right? Because-- - Yeah, yeah, exactly, exactly. - Anything that's worth really undertaking, academically speaking, is just, has to be outside of the average. - And our goal in life needs to be to be able to beat the averaging machine, to be able to have a thought that the averaging machine could not produce. Like, that becomes, that's our goal now. If all we're doing is what the averaging machine does, then we might as well be replaced by the averaging machine. Right, I mean, look, to be really clear, I wanna be, I don't wanna sound flippant here, right? I think people need jobs, people need employment, people get derived meaning from employment, and derive meaning from, you know, lives and families, and all those things. I'm not, yeah, I don't wanna come across as, like, some Silicon Valley bro here. But I think, like, at the same time, like, you know, our aspiration should be to be, like, we've gotta be able to do better than this. - I love it, I love it. I think this is a great point to finish the episode, because I think this was the most positive takeaway that I've had in a while, talking about LLMs.

[2:34:45] You know, like, this is, I think, I think there is a lot of room for maybe good things who actually come from it, you know? And that's good, that's great. - You know, my colleague, Will Crichton, he teaches a course called Tools for Thought, right? And he's trying to go back in this history of, like, tools for thinking. And that includes notation, like, prose. Just the act of writing was a tool for thought. Cuneiform was a tool for thought, right? Like, we've had tools for thought, calculators are tools for thought. But, so, if you understand the sweep of history, you know, mathematical notation was this amazing invention, right? There's actually this fabulous book from 1928 by Florian Kijori about, like, the history of mathematical notation. And there's people like Kenzie Kupreiter, who've written papers about, like, math notation, right? There's, like, amazing literature on all of these things about, like, diagramming. What is diagramming? Like, why do we sketch? What is the essence of a diagram? All these things are, like, tools for thought, right? So, instead of getting overwhelmed, I think if we think of, like, there's one more amazing tool for thought, right? Like, the same, this is a kind of different tool for thought, because the same tool for thought that is able to, like, you know, help me autocomplete my sentences, it also knows how to install Docker containers.

[2:35:56] That's kind of weird, right? That's not usual. So, that's a kind of weird tool for that. But it's, like, media, it's, like, okay at every one of these things. So, if we have this cognitive aid, what are the really interesting things we can do? Like, we've always, human cognition has always been, like, a limiting factor to various things. Because even once we have an idea, like, you know, I, for years I've told students this, right? It's, like, look, we sell this image of, like, you know, what is a PhD student, right? And, like, what is a PhD, what is research? And it's always, like, somebody's standing on a whiteboard, and there's, like, symbols on there. Like, every movie, right? There's, like, symbols on there. This person's, like, in a cloy, you know, like a white, you know, lab coat or something like that. And they say Eureka, and then, like, amazing things happen, right? Then, as I think it was Isaac Asimov who said, like, science happens not when somebody says Eureka, but when somebody says, hmm, that's weird, right? Like, then, and so, but also, you know, like, science is a collaborative, it's a human activity. It's, like, us sitting and talking to each other and, like, exchanging ideas and building on top of each other's ideas and doing all these other amazing things.

[2:36:59] And, but we've always struggled with, like, the limitations of it. It's, like, and I've always had told students, like, look, ideas are actually cheap, believe it or not. Like, you know, I have three ideas in the shower in the morning. Execution is hard. And I've seen students struggle with this because they've been led through these movies and all these other media thinking, oh, ideas, once I've had the idea, somebody else can execute it. It's, like, nobody, you're afraid to tell you, like, it's you, it's, the idea ain't even an idea till it's been executed and we've evaluated and found out whether it was an idea or not, right? So now, if we can have an accelerant for that process, right, you still have to take ownership. You still have to take responsibility. You can't, like, vibe code the idea. You have to, like, actually say that this is the thing I meant and these are the parameters and this is the study and this is how we're gonna evaluate it. But now you have a cognitive aid, a tool for thought for helping you debug it and work with it. And, you know, you don't only have to be with a human. You can do it with another machine as well, right? This is great.

[2:38:00] I think it's like, maybe this is all hype. Maybe all this stuff is gonna go away. Maybe we can't afford to run any of these things at all. Maybe we'll kill the planet. All these things are possible. But maybe also, in addition to all of those things, some really amazing things can happen because we've finally gotten, you know, the next generation, truly next generation of tools for thought. What a great world that would be if that were the case. - What a great world. I love it. - How's that a note to end on? - That was a great note. Yes, thank you. You are such a fabulous guest. It was, we barely had to do any work. Yeah. - It's your email. What are you talking about? You've done a ton of work. After you've done the work, it turns out you don't have to do very much work at all. You're right. Well done. Dan, Pedro, wonderful seeing you too. Thank you so much. Looking forward to running into you and let me know when the episode's on. - Is there anything that you didn't mention that you would like to talk about or like any final notes? - I don't think anyone needs to hear anything more from me. - We're always gonna hear a lot from you.

[2:39:03] Don't worry. - People will hear enough. There's no one here. - Awesome. Thank you so much. - Thank you so much, guys. (upbeat music) - After this conversation with Shreem, I went ahead and downloaded Claude. Got a big subscription. One of those hundred dollar bucks. A hundred bucks, one. And I started hacking around with it, seeing the power. And I must tell you, I was using Opus 5 and Fable. And I must tell you, it's, I was surprised. I was surprised. I think these things really change. Really change interactive three improvers that they use of it.

[2:40:06] I've been following all the hype, all the crazy stuff that is happening in the math community. But I hadn't been using these tools yet for formal verification. So I went ahead and I was tackling this verification of a small tiny compiler. So using kind of a concert like x86 semantics. I was surprised with the depth of proof search that it can perform. It's really incredible. And I think we are in the position where we can start, we can really start formally verifying real world software in the industry. You know, I foresee a rise of a new paradigm of software engineering. You know, together with testing, I believe that certain classes of programming, certain classes of applications of domains and of systems and programs, we can deliver with very robust proofs of their correctness.

[2:41:25] And I think this is feasible with the current AI age. And I believe that we're gonna start seeing a lot more companies tackling this field. I've started seeing some of them, started seeing companies hiring in this. And I decided that I wanna be part of this. And I started sending curriculums and talking with a couple of companies. So if you have a company or you work in a company that would be interested to try things out with formal methods or maybe start a formal methods team, let's be in touch. Let's be in touch. I have a message either on Twitter or send me an email. The email is Pedro@typethereforall.com or contact@typethereforall.com, doesn't matter. And let's talk, let's be in touch. I am very excited with making formal verification feasible for real world software. And two of the domains that I am the most excited about is compilers and blockchain and blockchain technology, particularly EVM sort of stuff, like smart contracts kind of things.

[2:42:41] Because that's also a kind of compiler. So I've been talking with some companies, but if you do have a company or you know someone or you're inside a company that would be interested in working with these things, let's be in touch, all right? And yeah, I know that I didn't, I usually leave this part to talk a little bit about the cast, about Shurum, but I'll leave that to Type There Exists. So that is gonna be Patreon. If you pay, I think $10 a month, you get access to another podcast basically, Type There Exists, where I talked about the behind the scenes, about the stuff that was happening, what's going on also in my life and like how my life interacts with the show and things like that. So I'll end this part with this invitation for you to become a patron, because I'm currently unemployed and I would really appreciate anyone's support. So that's it, go to the website typethereforall.com/patrons and become patron. See you guys next time.

[2:43:43] I love you all.