Richard Eisenberg on The Future of Programming

Richard Eisenberg — programming-languages researcher who spent years advancing Haskell’s type system before joining Jane Street — joins host Ron Minsky to explore what precise type systems can offer, what separates OCaml from Haskell in practice, and how AI-assisted coding changes the pressures on language design without making precise communication obsolete.

Key ideas

1. Dependent types let you encode a proof of correctness directly into your program, so the compiler checks it on every build. Where a normal type might say a function returns ‘a list of integers’, a dependent type can say it returns a list that is a permutation of the input in non-descending order — a specification so precise that any correct sorting algorithm satisfies it and any incorrect one cannot compile.
2. Unboxed types eliminate the hidden performance cost of OCaml’s uniform memory model. Today, even a 32-bit integer lives on the heap behind a pointer; accessing nested data means chasing a chain of pointers, each a potential cache miss. Unboxed types allow values to live directly in registers or on the stack, removing pointer indirection without sacrificing the type safety that makes OCaml productive.
3. The ‘pay-as-you-go’ principle governs good language design: powerful features should cost nothing when not used. Rust demonstrates the limit of the alternative — trading garbage collection for fine-grained memory control means every programmer pays the annotation burden all the time, regardless of whether their code needs that precision. OCaml’s goal is garbage collection by default and precise control where it matters.
4. Language design inside Jane Street gives OCaml features a rare testing ground before upstreaming. Open source languages face a brutal catch-22: release a feature to millions of users and discovering it was wrong is nearly impossible to fix. Jane Street can deploy an experimental feature firm-wide, run a ‘tree smash’ to change every call site at once when the design proves imperfect, and upstream only what has been battle-tested at scale.
5. AI-assisted coding raises the pressure to optimise for reading, not writing, and makes precise specifications more valuable, not less. When a model generates code, a human still has to read and trust it; a language that lets programmers write machine-checkable specifications gives AI output a verification layer. Eisenberg’s caution: if humans delegate writing the specification to the model too, they lose the ability to know whether the result is right.

Content

Background: from Pascal syntax diagrams to Haskell’s type system

Eisenberg’s path into programming languages is unusually self-made. At twelve he taught himself Pascal by staring for hours at the syntax reference — a set of block-and-line diagrams at the back of the compiler manual — with no glosses and no examples, on the assumption that the book must contain everything needed. That encounter built, he says, structures in his brain around syntax and formal language that shaped everything after.

An undergraduate course with Norman Ramsey lit him up formally, but arrived too late to redirect him immediately into graduate school. He taught high school for eight years before returning for a PhD at the University of Pennsylvania under Stephanie Weirich. There he discovered dependent types, began contributing to GHC (the main Haskell compiler — think of GHC as the single authoritative implementation, the way V8 is to JavaScript), and eventually became Chair of the Haskell Foundation and a member of the GHC Steering Committee, the body that governs how Haskell evolves.

He joined Jane Street after a stint at Bryn Mawr College — where open-source contributions counted as publications — and then at Tweag, a Haskell consultancy in Paris. Ron Minsky took eleven months to convince him; Eisenberg describes one of the barriers as a childhood vow never again to commute across the George Washington Bridge.

Dependent types: proofs baked into programs

A type is the contract a function advertises to its callers: this takes a list of integers and returns a list of integers. A dependent type extends that contract so the output can depend on the precise input — not just ‘a list of integers’ but ‘a list that is a permutation of the input list in non-descending order’. Any implementation that compiles is guaranteed to sort correctly; one that silently returns the empty list, which is technically a list of integers in non-descending order, cannot satisfy the richer type.

Eisenberg is careful not to oversell this. Proofs are expensive to write, and a good language makes their use optional. The cost–benefit question is whether the saved testing, debugging, and catastrophic-failure risk justifies the upfront precision. His answer: sometimes yes, sometimes no, and the programmer’s job is to apply taste about which parts of a system warrant the investment.

Ron Minsky raises the practical objection that automated theorem proving is notoriously labour-intensive — even expert users rely on tactic libraries and struggle with large proofs. Eisenberg agrees the tooling is immature, but argues the direction is right: languages like Coq, Agda, Idris, and Lean already embrace dependent types; OCaml’s module system, he notes, already has dependent-type characteristics, even if it is missing a few key features.

Unboxed types: paying for type safety at compile time, not runtime

OCaml’s memory model is, by design, brutally simple: everything is either a word-sized immediate value (a tagged integer) or a pointer to a heap block. This uniformity is what lets generic functions work without specialisation — List.map does not need to know what the list contains, because every element, whatever its actual type, looks like one word. The price is that a struct with four fields nested inside a larger struct means following four or five pointers to read a single value, with a probable cache miss at every step.

Unboxed types (a term Eisenberg explains as ‘inlining of type definitions’) allow values to live directly in memory — in registers, on the stack, or flat inside larger structures — without pointer indirection. The complication is polymorphism: once types differ in their physical layout, a single function cannot walk them uniformly. OCaml’s current best answer is to specialise at compile time, generating different machine code for different layouts, much as C++ templates do.

The interaction with polymorphism (the ability to write one function that works for any type) deserves unpacking. OCaml today can write a function polymorphic over ‘any type’, because every type occupies one word. Once unboxed types introduce layouts of different sizes, ‘any type’ must be refined to ‘any type of this layout’, and some polymorphic functions may need separate compiled versions for each layout that calls them. Eisenberg describes this as the central unsolved design challenge, and one he does not believe any other language has tackled in quite the same way.

OCaml versus Haskell: what each language makes explicit

Eisenberg has worked in both ecosystems simultaneously since joining Jane Street, which makes his comparison unusually grounded. Two contrasts stand out.

First, Haskell favours compile-time explicitness; OCaml favours runtime explicitness. Haskell programmers routinely write type signatures beside every function — a discipline that doubles as documentation and makes it natural to add prose comments nearby. OCaml separates interface files (which carry types) from implementation files (which carry code), and the distance tends to mean less documentation on the implementation side. Minsky questions whether this is a language property or a cultural one; Eisenberg concedes it may be both.

Second, Haskell’s lazy evaluation — where let x = big_computation defers big_computation until x is actually used — makes Haskell’s compiler optimise more aggressively but makes performance harder to predict. OCaml evaluates eagerly: expressions are computed in the order they appear, making runtime behaviour more transparent.

Third, typeclasses — Haskell’s mechanism for overloading a single name to mean different things for different types (similar to how + can add integers or floats) — are powerful but create dense, hard-to-read code when many overloaded names appear together. OCaml is more explicit about which operation is being called, at the cost of some verbosity.

Language extensions: Haskell’s 2¹⁵⁰ dialects

Haskell accumulated roughly 150 compiler extensions because it began as a committee language with multiple competing implementations: if one compiler wanted to try a new feature, it could label it an extension so the other compilers could keep ignoring it. GHC is now the only live implementation, but the extension mechanism remained and multiplied. The result is that a newcomer opening a Haskell file sees a list of twenty extensions at the top and cannot tell which are experimental, which are decades old, and which are known to be dangerous.

Eisenberg, as a GHC Steering Committee member, wants to rationalise this — reducing 150 extensions to perhaps seven, with a clear notion of a standard language that most programmers use, whilst preserving backward compatibility for files already relying on existing extension names. He does not expect to get all the way to one language, but thinks 80% consolidation is achievable.

OCaml, by contrast, is conservative and un-extensioned: close to one standard language, one compiler, one set of rules.

AI-assisted programming and the future of language design

Minsky introduces the question Eisenberg has clearly been asked many times: does the rise of large language models — systems that can generate plausible code from a natural-language prompt — change what programming languages need to be?

Eisenberg’s answer is evolutionary, not revolutionary. A programming language is, at its core, a medium of precise communication — from human to computer, and from human to human. AI adds a third channel: computer to human, in that generated code must be read and verified by its recipient. This does not remove the need for precision; it increases it.

His maxim is that language design should optimise for reading, not writing, because code is read far more often than it is written. If AI does more and more of the writing, that pressure intensifies: the generated code must be easy for a human to audit, and a machine-checkable specification (dependent types, refinement types, or something similar) gives the auditor a formal target to compare against the implementation.

The scenario he finds genuinely dangerous: asking the model to write both the specification and the implementation. If the human cannot independently evaluate whether the specification is correct, the loop is closed — the model can produce whatever it likes and there is no check. Eisenberg is explicit that this is where the system breaks down, and that preserving human ability to read and judge precise specifications is not an optional luxury.

On timeline, he is measured: too early, in May 2023, to design a language from scratch for this mode of interaction, given how fast the models are changing. In two years, perhaps. The better near-term starting point is languages already built for precise communication — because that is, in the end, what the interaction still requires.

Related

• Richard Eisenberg — speaker
• Ron Minsky — host
• Stephen Dolan on Memory Management, Garbage Collection, and OCaml — companion Signals and Threads episode; Dolan covers the memory-management substrate (local types, unboxed types) that Eisenberg works on from the type-system side
• Leo White on Language Design — earlier Signals and Threads episode on OCaml’s design philosophy and the road to dependent types
• The Future of Software Engineering — theme; the conversation sits squarely in the question of how programming evolves under AI pressure