PL Education in the Age of AI

A two-and-three-quarter-hour interview with Shriram Krishnamurthi, the Brown professor behind Pyret, the Bootstrap curriculum and a long list of Racket-based teaching material. The episode is an audio podcast, so video_id holds the audio file's id (the same one the transcript carries) and there are no deep links: timestamps below are positions in the recording. The conversation starts with how he came to programming languages and ends up on what a computer science department is for once agents write the code. One position runs through all of it. The people who care most about a subject make poor judges of how to teach it, because they design for students like themselves, and the same blind spot is what makes current opinions about AI in education close to worthless.

The argument

Expressiveness, and the part PL won't admit is emotional

His route into the field went through Matthias Felleisen's paper On the Expressive Power of Programming Languages, which he read as a grad student bailing out of computational biology [13:48]. What he admires is that it takes a question everyone treats as opinion ("are generators more powerful than async?") and refuses the Turing-completeness shrug. A feature adds no expressive power if a local macro can rewrite it away, the way for rewrites to while; the paper then shows that some features, mutation and continuations among them, cannot be rewritten that way [16:57]–[18:06]. He built his Papers We Love talk around it, and chose it partly because it was the least cited of his candidates [20:21].

Against that mathematical instinct he sets the claim that people have emotional reactions to languages and the field does not want to acknowledge them [21:24]. His own is a love of parenthesized syntax, which he compares to being left-handed: a stable minority of ten or fifteen percent that the world is not built for [22:40]–[23:44]. Pyret exists, by his account, mostly to take syntax off the table, because every conversation with educators about his pedagogic ideas stalled on the parentheses [23:44]–[25:57]. He does not treat that as a failing of the listeners. Learners focus on what is most visible, which he calls superficial in the literal sense of on the surface, and educators meeting a new language are learners too [24:54]. Paul Graham's Blub paradox is his model for everyone's language preferences, his own included [27:01].

On design he offers two principles. Every language is domain-specific whether it admits it or not: COBOL, FORTRAN, ALGOL and LISP are named after their domains, and "general purpose" means a comfortable middle of web and desktop programs that don't need to scale [28:07]–[29:11]. So let the domain push on the design, then find the computational medium that fits it. The second principle comes from his misconception research: design the language, the IDE and the error messages so they avoid misconceptions or make them surface [30:15].

The dynamic-programming aside is the most concrete example in the episode of "how you say it matters." Most algorithms books go straight to the two-dimensional table, and LLMs asked about dynamic programming do the same. He prefers teaching memoization first, which exposes the actual idea: repeated subproblems that always return the same answer, so the answer can be stored in a space-time trade. Dynamic programming is then the bottom-up rewrite, and the memoized version is the oracle for checking it [34:46]–[37:55]. The matrix, he says, comes from textbook examples like edit distance that happen to take two string-like arguments, and has nothing to do with the technique.

He also names the unstated language of those books. SMoL, the Standard Model of Languages (the transcript spells it "small"), is the semantic core shared by Java, C#, Python, JavaScript, Racket and OCaml but not Haskell or Prolog: first-class functions, mutation, garbage collection, references passed rather than values copied [32:34]–[33:43]. It is built into big-O itself, since assuming a function call costs one unit of time already assumes arguments are not copied [39:59]. He calls it a decent design the field reached by trial, including a retreat from variable aliasing once swap turned out to matter less than the bugs it caused [41:00]–[42:02].

Designing for the other 90%

His teaching philosophy starts from a complaint about academics: "one of the things academics are really good at is producing clones of ourselves" [47:38]. Feedback comes from the students most like the teacher, who say the course changed their lives, and nobody hears from the rest. The insight came from advising a PL-minded student to take a machine learning course. What he wanted from that course was a service course that gave a non-specialist a working toolkit, so he asked why his own PL course should be any different [48:43]–[50:53]. The ten percent who will become researchers will be fine whatever is taught. Undergraduate courses, including the formal methods courses Brown added, are designed for the other ninety; the graduate course is where he goes all in on theory [50:53]–[52:08].

That changes grading as well as content. He stopped doing mastery learning for the undergraduate course, split assignments into essential ones and aspirational ones, and tells pass/fail students to nail the essentials and skip the rest, because fifty percent across the board just means being bad at everything [55:19]–[57:21]. Writing a type checker is essential; Hindley-Milner inference is "one of the most beautiful algorithms in the history of computer science," and still optional [57:21].

His PL course runs four threads [52:08]–[54:16]. One corrects misconceptions about SMoL, since that is what students will program in. One asks where language designs come from. One has students implement the essence of an interpreter or a type checker, so these stop being mysterious. The last relates the course to the outside world: a tweet about a confusing program, an article about goroutines, error message design, and why keywords are English. One student built a Racket with Thai keywords so he could teach his mother to program [54:16].

He is also explicit that half the point of a PL class is inspiration. "I think we spend too much time in PL worrying about like preventing things and not enough time about like enabling things" [1:03:02]. He demos FrTime and Prolog in class for the moment a student realizes a language can do that [1:04:06].

Why Racket

Asked why Racket, he explains #lang through the shebang line: the first line of a file decides the syntax and semantics of the rest [1:06:11]. That makes Racket a machine for defining languages. His course needs roughly thirty languages for the mystery-language exercises alone. Students get one syntax with several implementations behind it: typing 5 + 7 prints 12 three times, and the job is to write programs that tell the implementations apart, such as a division by zero or 0.1 + 0.2. Each variant corresponds to semantics real programmers have had to deal with [1:09:24]–[1:10:31]. The one language not used in class is plain #lang racket [1:10:31].

Two things matter more to him than the parentheses. Uniform syntax lets students focus on semantic differences, which he grounds in cognitive science: people learn from variation, so hold everything else constant [1:12:44]. And the languages are restricted, not just conventional. The first example language has only strings and concatenation, and typing 3 is an error. Students "always screw up the conventions," and the cost is not lost credit but a missed learning objective [1:15:58]–[1:17:03]. When a host suggests monads could do the same job, his answer is that monads parameterize a language but cannot take the rest of it away [1:14:52]. He would like to see the approach rebuilt in another system, perhaps Lean, and says he doesn't know how to restrict the language there [1:19:20]. Matthew Flatt's Rhombus is under consideration for an infix version [1:11:36].

Truth, proof, confidence

The type-theory host's question is whether undergraduates should meet proof assistants. Krishnamurthi's answer: "I actually don't think most people care about proof" [1:20:23]. Most people have trouble caring whether something is true, and truth and proof are different things [1:21:25]. From his grad-school formal methods training he draws three lessons (everything comes down to finite model theory; automated methods and model checking; the value is in finding bugs) and one from Daniel Jackson: before investing in a proof, find out whether the thing might be true [1:22:29].

He speaks as someone who has done the proofs, including an early type-soundness proof for Java [1:23:36], and his objection is to what they are about. A theorem is about a model, and the bugs live in the gap between the model and the thing. The JavaScript work with Arjun Guha insisted that the model match what browsers do, because a sandboxing theorem is proved against an adversary, and no adversary declines an exploit for not fitting your model [1:24:39]. What people actually want is confidence. His group's semantic-differencing work reframes change as a confidence problem: a system that has been tested and used for six months is trusted, a fix or feature arrives, and the question is how to "transfer my confidence in the old thing to the new thing" [1:26:48]–[1:27:54]. He adds that PL proves safety properties because the tools make them easy, and misses the wider family of properties he learned about in verification [1:27:54].

On agents generating proofs he is "optimistic, but also wary" [1:29:02]. Push-button tools like SAT solvers and model checkers require no knowledge of what happens inside. A failed LLM proof search gives a beginner a long trace and no statement that the goal is false, so the missing piece is a human-factors research problem: surfacing the failure so a domain expert can steer [1:30:08]–[1:31:10]. He closes the topic with legitimate peripheral participation, the sociological account of how people move from the edge of a community to its center. Good intentions about growing a community are necessary and nowhere near sufficient without it [1:34:22]–[1:36:27].

What agents did to the feedback loop

Pressed on whether agents should push proof assistants earlier in the curriculum, he says he doesn't know, and insists the distinction matters: he has opinions, but not knowledge [1:38:32]–[1:39:41]. His complaint about computing education research is a mismatch in rigor. A compiler paper evaluated by asking the colleague next door would be humiliating, yet most education work is evaluated that way. "Why don't we bring the same rigor to our educational work as we do to our research work?" [1:41:55]. Without real experiments, people who love Lean will find that Lean works and people who hate it will find that it doesn't [1:43:00].

What he did instead was run a course. He came back from winter break converted to Claude, and a colleague stopped him from simply trying something in the intro courses. She pointed to the expert blind spot: instructors cannot put themselves in a novice's place, so the only way forward was to watch real novices [1:44:04]–[1:45:15]. The spring course had all coding done with Claude Code on a deliberately limited $20 subscription, so the rate limit would stop students from spending every waking hour on it [1:46:16]. The students had minimal but nonzero programming experience, in case they ever had to read the code, and every assignment came with a reflection journal written by hand [1:47:20]. Findings go up on the course page as the analysis proceeds, and the intro courses are being redesigned from them [1:48:22].

The first finding is about feedback. Before agents, an assignment that was too hard showed up in office hours, on the forum, in missed submissions and in tired faces. Now "all of our previous channels for feedback no longer work," because Claude can build anything an early course assigns, with a finished interface and no understanding on the student's side [1:49:24]–[1:50:28]. The Matrix chat-client assignment showed the second. He had checked for hours that Claude knew Matrix well, but that check relied on forty years of knowing what to ask. Many students did not know what question to ask, or how to make sense of the three paragraphs that came back [1:51:31]–[1:52:34]. And a student who asks Claude instead of posting on the forum removes the very signal instructors needed [1:53:37].

Asked how that makes him feel, he tells the story of his first CHI conference, where he knew nobody and had lower status than the grad students, and felt more alive for it. He had learned new fields before and would again [1:53:37]–[1:55:52]. He expects a wave of bad vibe-coded systems, and he watches himself for the regressive urge to insist his forty years must matter [1:56:57].

What a computer science department is for

The priesthood has lost its monopoly on the hieroglyphics. What is left is quality: "We have to be the people who are the bastions of quality" [1:59:08]. He leans on Parnas's keynote "Software Engineering: An Unconsummated Marriage": engineered products come with warranties, software comes with disclaimers, and a one-dollar plastic product can be returned while a million-dollar program points you to the license you accepted [1:59:08]–[2:00:10]. Teaching students to stand behind a product is the value a department can offer, and to him it is the long-awaited moment for formal methods [2:01:21].

He has little sympathy for CS1 instructors mourning their factorial exercises. They have long said they teach problem solving rather than programming, and now programming is the trivial part, so they can finally do it. A colleague's line: you can't claim to teach problem solving just because you give students a lot of problems to solve [2:01:21]. He also brings up Grace Hopper, who was told her compiler could not exist and then spent decades being laughed at for wanting programming to look like natural language. He wishes she were alive to see it [2:02:23]–[2:03:38]. The concrete curriculum he sketches is about test generation: tests generated alongside the code are "also known as a correlated failure," so students should learn to elicit properties and hand them to model checkers, model finders or proof assistants [2:03:38]–[2:04:41].

Writing as thinking

The last hour is about writing. He studied humanities alongside computer science and found the same rigor there, starting with a professor who called out his attempt to bluff through a reading [2:05:44]–[2:06:48]. His PhD advisor spent two or three years convincing him he could not write, then rebuilt his writing. Having come up in India on a flowery school style, he now tells his own students they will learn his style first and find their own voice later [2:07:52]–[2:08:55]. His papers start from a worked example, go from concrete to abstract, and now state findings in the abstract instead of saving them for page seventeen [2:11:07], [2:15:32]. Writing styles are another Blub: scientists, lawyers and PL researchers each find the others' conventions bizarre [2:15:32]. He teaches writing by sitting beside a student and spending an hour on one paragraph, asking before each sentence what the student thinks he will say, so they build a classifier in their heads [2:19:48]–[2:20:51].

The LLM question gets the same answer as the programming one. Writing is "a foundational form of thinking," and he compares it to the gym: once physical labor stopped supplying exercise, people had to seek it deliberately [2:24:10]–[2:25:15]. He would let Claude do routine revisions to curriculum text and review every diff down to the character, but he has never published a sentence an LLM wrote. The six-page memo in which he asked why programming languages matter once agents write the code was typed entirely by him: "I cannot imagine substituting even a character of that thinking with an LLM" [2:26:23]–[2:29:59]. The contrast he draws is that programming today is tedious while writing is hard, "and I wanna do hard things, not tedious things" [2:29:59].

The episode ties this back to where it started: with LLMs, the scaffolding is macros, and the part that is not a macro has to come from the author [2:31:25]–[2:32:27]. His test for any statement a university or company publishes is whether it says anything an LLM would not have said. If the text is the statistical mean, send the prompt instead. His practical version is to list your points, ask a model for three paragraphs on the topic, and keep only the points it missed [2:32:27]. "Our goal in life needs to be to be able to beat the averaging machine" [2:33:37], and he adds straight away that he doesn't mean to be flippant about people who need jobs. He closes on Will Crichton's tools-for-thought course: notation and writing were tools for thought, and this one is strange because the same tool that completes his sentences also installs Docker containers [2:34:45]–[2:35:56].

In a coda recorded after the interview, host Pedro reports trying Claude on verifying a small compiler. He was surprised by how deep its proof search went, and now expects formal verification of real-world software to become feasible [2:39:03]–[2:40:06]. Next to Krishnamurthi's wariness about the failure path, that is the other side of the same bet.

Quotes worth keeping

• "I think we spend too much time in PL worrying about like preventing things and not enough time about like enabling things" [1:03:02]
• "It's hard enough to get people to care about whether something is even true. Forget about proof" [1:21:25]
• "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." [1:24:39]
• "How can I transfer my confidence in the old thing to the new thing?" [1:26:48]
• "Why don't we bring the same rigor to our educational work as we do to our research work?" [1:41:55]
• "All of our previous channels for feedback no longer work." [1:50:28]
• "What is left is quality, right? We have to be the people who are the bastions of quality." [1:59:08]
• "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." [2:29:59]
• "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." [2:33:37]

Relation to other pages

dont-outsource-learning reports that engineers who asked a model conceptual questions kept their comprehension while those who pasted its code lost it, and prescribes asking for the explanation first. The Matrix assignment is the case that advice assumes away: novices who could not form the conceptual question, and could not parse the answer when they did. Osmani's reader already knows enough to ask. Krishnamurthi's students did not, and his course is an attempt to measure what happens then instead of guessing.

The statistical-mean test is the writer's version of llm-as-average-democratizer. That page argues that once average output is cheap, average stops being worth anything. Krishnamurthi turns it into a working rule: a text that sits at the mean should be replaced by its prompt, and only the points a model leaves out are worth writing down.

On proofs, zstd-lean-proof-automation shows the success path he is optimistic about, with a nontrivial theorem proved by LLMs in twenty minutes. His wariness is about the failure path Langley barely exercised: when no proof is found there is no counterexample, and nothing a non-expert can act on. The host's coda sits closer to Langley.

The Parnas warranty argument meets resistance in we-are-not-special, where Hillel Wayne's crossover engineers found software keeping better records and running more verification than traditional engineering. Both can be true. Parnas is talking about the accountability a product carries to its buyer, and Wayne's interviewees about practice inside the team. The claim that what remains for programmers is quality and responsibility is the curricular counterpart of recall-to-judgment. The gym comparison for writing is the same mechanism ironies-of-automation describes for operators: automating a task removes the practice that kept people able to do it.

know-thine-enemy is another computing-education academic's experiment with Claude Code. Amy Ko ran hers on herself for three months, while Krishnamurthi ran a course and collected handwritten journals, which is closer to the kind of evidence he says the field lacks.

The transcript in pl-education-in-the-age-of-ai-transcript is a local whisper run over the audio and has not been checked against it. Whisper mangled most proper names ("pirate" for Pyret, "small" for SMoL), so names on this page were matched against context, and anything uncertain was paraphrased rather than quoted.