May 18, 2023, 11:34 AM ETInterview, Fireside Chat

The Future of Programming with Richard Eisenberg

Richard Eisenberg joined Jane Street as a senior contributor to the tools and compilers team, specifically leading work on the front end of the OCaml compiler.
Eisenberg previously spent eight years in the Haskell ecosystem, contributing to the type system, serving on the GHC steering committee, and chairing the Haskell Foundation.
He transitioned from a PhD in programming languages and a professorship at Bryn Mawr College to Jane Street after being convinced over an 11-month period to leave the Haskell space.

Dependent types allow programmers to encode proofs of correctness directly into program types, ensuring the compiler verifies properties (e.g., that a sort function returns a permutation of the input) at compile time.
Eisenberg advocates for a "pay-as-you-go" approach where powerful features like dependent types are opt-in to avoid forcing all programmers to handle the complexity of theorem proving.
He notes that while tools like Coq, Agda, Idris, and Lean embrace dependent types, languages like OCaml and Haskell only partially support them without forcing their use.
The practical application of dependent types requires a cost-benefit analysis: the time spent writing proofs should yield savings in testing, debugging, or avoiding catastrophic failures.

Eisenberg's current mission is to design "unbox types" for OCaml, a feature allowing the inlining of type definitions to eliminate runtime pointer indirections and cache misses.
Current OCaml memory representation separates heap-allocated values (with headers and pointers) from immediate values, causing performance penalties when nesting data structures; unbox types aim to make this distinction explicit in the type system.
This shift requires making performance engineering decisions (e.g., memory layout) visible in the type system, contrasting with the "compiler optimization" approach of hiding these details.
A significant trade-off of unbox types is that they interfere with parametric polymorphism, potentially requiring compile-time code generation to support polymorphic functions with unboxed data.
The team plans to test a compiler flag to explicitly disable boxing, offering a path toward fine-grained memory control similar to Rust but retaining OCaml's garbage collection.
Unlike Rust, which forces manual memory management for all code, OCaml will maintain uniform memory management as the default while offering explicit control where needed.

Jane Street iterates on language features internally using "tree smash" refactoring tools to change codebases wholesale, allowing them to fix design flaws before proposing upstream changes.
This internal incubation phase allows the team to validate designs under real-world constraints before engaging the broader open-source community to prevent breaking thousands of external users' programs.
The team seeks external feedback early via public presentations to avoid "overfitting" features specifically to Jane Street's internal coding styles and needs.
Jane Street views itself as a significant contributor to the open-source OCaml ecosystem, which is rooted in Inria (France), and aims to upstream features like unbox types once they are battle-tested.
Upstreaming OCaml changes requires consensus with the broader community, as Jane Street does not own the language.

Documentation & Interfaces: Haskell typically embeds type signatures and documentation near functions, whereas OCaml separates interface files from implementations, often resulting in less in-code documentation.
Runtime Semantics: OCaml is eager and explicit about runtime behavior, making performance prediction easier; Haskell is lazy, offering aggressive compile-time optimization but making runtime performance harder to predict.
Type Classes: Haskell uses type classes to allow multiple definitions for a single function name (ad-hoc polymorphism), which can reduce code readability; OCaml requires explicit function naming, making operations more obvious.
Language Evolution: OCaml is highly conservative with a single compiler (OCaml) and no official standard, limiting feature proliferation; Haskell historically relied on multiple compilers and over 150 optional extensions, creating a fragmented ecosystem that is now consolidating around the Glasgow Haskell Compiler (GHC).
GHC Steering Committee is currently debating restructuring the 150+ language extensions into a smaller, unified set of ~7 core features to improve usability while maintaining backward compatibility.

Eisenberg views AI-assisted programming (e.g., LLMs) as a significant step that increases pressure on language design to optimize for "reading" rather than "writing."
Precise communication remains critical; LLMs are fallible, so specifications must be explicit enough for humans to verify correctness if the computer generates the code.
Dependent types could serve as a precise input language for LLMs, allowing models to generate code that meets formal specifications (e.g., "sort a list into a permutation in non-decreasing order").
There is a risk that if humans rely entirely on AI to write both specifications and implementations, they lose the ability to validate the "what" vs. the "how," rendering the system unverifiable.
Eisenberg suggests that while future language designs might accommodate AI interactions, current designs for precise communication (like Haskell and OCaml) remain the best starting point for the foreseeable future.