My Argument for Teaching Intro CS in Lean 4

A disclaimer: this post isn’t entirely serious; unfortunately I do not believe we should immediately refactor UW’s intro courses to only use Lean 4. It started as a joke talk at the 2026 PLSE kickoff, and it’s my own attempt to persuade you, dear reader, to switch your intro CS course to be taught in Lean. I won’t be giving the counterarguments justice. Here at UW, the wonderfully designed CSE 12X intro courses are taught in Java, so Java is the language I’ll use as a baseline for the rest of this post. I’m a PhD student, not an educator; I am interested in hearing your serious and unserious thoughts on this, especially if you’re more knowledgeable than me!

Lean is a dependently typed programming language that’s best known as a proof assistant: a way to encode logical propositions (like “the primes are infinite”), write down proofs of those propositions as programs, and typecheck those proof-programs to verify their legitimacy. This works because of the Curry-Howard correspondence, which connects types to formulas and programs to proofs. Lean, like all other proof assistants I know of, is quite difficult to learn.

I recently had the pleasure of TAing an intensive 3-day Lean workshop full of wonderful math faculty members from the Pacific Northwest, sponsored by PIMS. For some attendees, it was their first time programming; I learned a lot about what it’s like to learn Lean.

My proposal is to forgo dependent types and proofs in an intro course, and only use Lean as a functional programming language. When I started with Lean, I was surprised to learn that Lean 4 supports a version of most of the concepts a typical intro course covers today: IO, reassignable variables, loops, and programs you can run from the command line. Here’s a program that reads natural numbers from standard input, one per line, until it gets a line that isn’t a natural number. Then it prints how many numbers it read and their sum:

def main : IO Unit := do
  let stdin <- IO.getStdin
  let mut counter := 0
  let mut sum := 0
  while true do
    let line <- stdin.getLine
    match line.trimAscii.toNat? with
    | some n =>
      sum := sum + n
      counter := counter + 1
    | none => break
  IO.println s!"{counter} numbers, summing to {sum}"

There’s a while loop, a break, and variables declared with let mut that get reassigned inside the loop¹. The match handles the case where toNat? fails to parse a line as a number, which is how the loop knows to stop. It doesn’t use any of Lean’s fancy but sometimes scary Unicode operators, either! When programming, you can largely avoid typing them; when proving, they’re fairly important for making mathematical formulas compressed and recognizable for humans to read.

Why Lean 4 is my choice for intro

Evens out the playing field

Some students enter their undergraduate years with no coding experience. Others have taken AP CS courses and are itching to skip one or more intro CS courses because they’re already comfortable with Java’s syntax and basic control flow. UW currently uses a guided self-assessment to find the right course for each student.

If you teach intro in Lean, everyone’s on equal footing from the get-go:

How convenient!

Types specify code

Intro CS courses are meant to teach students how to predict and simulate the behavior of programs. In a language like Java, that can be difficult without using second-class documentation:

User lookup(int id); // can this return null?
Config parse(String s); // does this throw an exception?
int total(int[] xs); // can this overflow?

I believe that we should teach students a first language that encourages them to document behavior like this upfront. Java does have Optional and checked exceptions, but they aren’t part of the least-friction way to write Java code. Here are the analogous signatures in Lean 4:

lookup (id : Nat) : Option User
parse (s : String) : Except String Config
total (xs : List Int) : Int

In Lean, pure functions report expected failure in their types: Option User encodes the fact that lookup may not find a user, and the caller must handle the none case. Functions with a ! suffix, like head!, panic instead: by default they print an error and carry on with a default value which keeps them total; Lean can also be configured to abort on panic. Likewise, parse returns an Except String Config, which is either an error message or a Config. And Int is an unbounded integer, so total cannot overflow. Fixed-width types like UInt64 still wrap around silently, though.

Each of Lean’s least-friction decisions here favors expressing possible failures upfront or eliminating them². This can certainly make it a less practical real-world language, but a simple model with fewer hidden gotchas is easier to learn.

Lean leads with transparent data types

I clicked “Go to Definition” on Java’s ArrayList, and here’s where it brought me:

public class ArrayList<E> extends AbstractList<E> implements List<E>, RandomAccess, Cloneable, Serializable {
   private static final long serialVersionUID = 8683452581122892189L;
   private static final int DEFAULT_CAPACITY = 10;
   private static final Object[] EMPTY_ELEMENTDATA = new Object[0];
   private static final Object[] DEFAULTCAPACITY_EMPTY_ELEMENTDATA = new Object[0];
   transient Object[] elementData;
   private int size;

   public ArrayList(int initialCapacity) {
      if (initialCapacity > 0) {
         this.elementData = new Object[initialCapacity];
      } else {
         if (initialCapacity != 0) {
            throw new IllegalArgumentException("Illegal Capacity: " + initialCapacity);
         }

         this.elementData = EMPTY_ELEMENTDATA;
      }

   }

   public ArrayList() {
      this.elementData = DEFAULTCAPACITY_EMPTY_ELEMENTDATA;
   }
   ...

I remember the abject horror this brought me when I was learning Java: what are all these private static final fields? What could transient mean? Before we even get to adding an element, there’s a serial version number, two different empty arrays, a default capacity, and an exception for negative capacities. Compare that to List and Array from Lean. Here are their definitions:

inductive List (α : Type u) where
  /-- The empty list, usually written `[]`. -/
  | nil : List α
  /--
  The list whose first element is `head`, where `tail` is
  the rest of the list. Usually written `head :: tail`.
  -/
  | cons (head : α) (tail : List α) : List α

structure Array (α : Type u) where
  /--
  Converts a `List α` into an `Array α`.

  The function `List.toArray` is preferred.

  At runtime, this constructor is overridden by
  `List.toArrayImpl` and is `O(n)` in the length of the
  list.
  -/
  mk ::
  /--
  Converts an `Array α` into a `List α` that contains the
  same elements in the same order.

  At runtime, this is implemented by `Array.toListImpl` and
  is `O(n)` in the length of the array.
  -/
  toList : List α

A List is either empty (nil) or an element stuck onto the front of another list (cons). An Array appears to be³ just a wrapper around a List. Admittedly, the universe u is its own horror that has escaped from the world of type theory, but I do believe its presence is less disturbing than ArrayList’s boilerplate.

Instructors can write custom, simple Java types for students instead, but then the course loses the educational advantage of interacting with a language’s base library.

Lean leads with simple APIs and data structures because of its primary goal of proving facts about its data structures. That simplicity also serves pedagogy.

Natural recursive functions

Recursion is a troublesome beast to tackle in an intro CS curriculum. Here’s a flawed Java method that sums up a custom singly linked list whose last node has a null node.next pointer:

private int sum(LinkedNode node) {
    return node.data + sum(node.next);
}

It always calls sum on node.next, so once it reaches the end of the list, node is null and we get a NullPointerException. This is a common recursion mistake when programming without exhaustive pattern matching: the author got the recursive step correct, but failed to account for the base case. Unfortunately, Java is perfectly happy to compile this. Here’s a similar mistake in Lean: a function on List Nat that handles the cons case (x :: xs) but forgets about the empty list ([]):

def sum : List Nat -> Nat
  | x :: xs => x + sum xs
  -- Missing cases: []

The language server puts a red squiggle under the pattern match, and the error points out what’s missing: Missing cases: []. The student finds out about the bug before they ever run the code, and they receive actionable feedback on how to resolve the issue. Functional programming languages encourage recursive functions’ cases to mirror the shape of their data, and Lean enforces that with an error.

A caveat is that Lean also requires its functions to be terminating by default, and sometimes its termination checker needs help in the form of a proof, which we aren’t trying to teach in an intro class. The termination check can be sidestepped with partial def, which removes the termination guarantee. The downside of partial def is that proofs cannot unfold such definitions, which isn’t a problem in our hypothetical proof-free course.

Lean is customizable

Lean 4 has user-extensible syntax, elaboration (type-aware desugaring), and linting. There are multiple teaching projects in the wild that have customized Lean’s proof system to teach theorem proving to beginners, such as Verbose Lean, the Lean Game Server, and The Mechanics of Proof. Racket’s teaching dialects make great use of Racket’s extensibility. For example, they leave out higher-order functions until later levels. This lets Racket’s IDE report common beginner mistakes, like balanced but misplaced parentheses, with helpful errors. Lean 4 isn’t as extensible as Racket is, but some of Lean’s sharp corners can be rounded off in this way.

Here’s a Lean snippet that forbids the use of anonymous functions declared with fun. I’ve used the macro system to override how fun is expanded; I could also have registered a custom linter, which has the added benefit of being able to inspect types (for example, not allowing functions to be passed as arguments).

open Lean in
@[macro Lean.Parser.Term.fun] def noLambdas : Macro :=
  fun stx => match stx.getHeadInfo with
  | .original .. => Macro.throwError
      "No `fun` allowed in this course!"
  | _ => Macro.throwUnsupported -- pass through this macro

def double (n : Nat) : Nat := 2 * n

#eval [1, 2, 3].map double -- works
#eval [1, 2, 3].map (fun n => 2 * n) -- fails

Commands like #check, #eval, and #guard are ergonomic for experimenting

Lean 4 has the commands #check, #eval, and #guard that you can drop anywhere in a file. The #check and #eval commands output the type and result of an expression respectively, and #guard operates as a unit test:

def sum : List Nat -> Nat
  | [] => 0
  | x :: xs => x + sum xs

#check sum -- sum : List Nat → Nat
#eval sum [1, 2, 3] -- 6
#guard sum [1, 2, 3] = 6
#guard sum [] = 0
#guard sum [] = 1 -- fails

These commands run at elaboration time, so they run live in an IDE. The commands don’t affect the rest of the file’s elaboration. Lean makes it very easy to insert #check and #eval as a cheap debugging tool, and #guard makes unit tests visible, hard to forget about, and easy to modify and extend. The results show up right in the editor as the student types, similar to a Jupyter notebook that reruns every cell below your edit, so there’s no hidden state.

Why not use another functional programming language?

Most of the arguments I presented for Lean 4 support strongly typed functional programming languages like SML or Haskell as much as they support Lean. After all, I am proposing to skirt around Lean’s dependent typing and theorem proving. The advantage Lean 4 has over traditional FP languages is that Lean can better serve the curriculum of later classes. I believe that teaching students the basics of programming in Lean will lower the barrier to its more challenging topics: students will already be familiar with its expression syntax and execution model. If students have seen Lean before, it becomes a lot more feasible to teach basic theorem proving in the logic/discrete math class. After all, if we rework intro CS to be in Lean, it only makes sense to rework the rest of the curriculum too, right? How hard could it be?

I managed to go almost an entire blog post without mentioning LLMs in 2026, but many people, including myself, believe that the unreliability of LLMs pairs very well with the guarantees that a proof assistant can offer. I wouldn’t be surprised to see dependent typing and theorem proving become more widely adopted and sought after in industry as verification becomes cheaper.

Acknowledgments

Thanks to Zach Tatlock for seeding this idea and Matt Wang for the encouragement to turn this into a blog post. Thanks to PIMS for sponsoring the Lean workshop and Eric Klavins for teaching UW’s Lean course and running the workshop.