The language that says no

In the 1970s Robin Milner, a computer scientist at the University of Edinburgh, was working on LCF, a program to check mathematical proofs, and it became one of the three achievements his Turing Award named in 1991. Asked about it in a 2003 interview, he described a night at the computer:

So if you stayed late at night working out a proof with the computer, you wouldn’t have to think afterwards “gosh, did I cut a few corners?”, because the LCF system just wouldn’t have allowed you to do so!

Fifty years on, the one up all night at the computer is an agent, and it cuts corners.

In LCF, proofs were driven by small programs Milner called “tactics”, which could be clever, sloppy or plain wrong. A theorem was an abstract type, thm, whose only operations were the rules of inference, and “strict typechecking then ensured that the only values that could be created were those that could be obtained from axioms by applying a sequence of inference rules – namely theorems.”¹1Michael J. C. Gordon, From LCF to HOL: a short history, in Proof, Language, and Interaction, MIT Press, 2000. And David MacQueen, Robert Harper and John Reppy, The History of Standard ML, HOPL IV, 2020. A tactic could fail, loop or give up, and still could not hand you a false theorem, because no such value could be built. The language he designed to write the tactics in was called ML, the MetaLanguage, and OCaml is what it grew into.

From LCF to OCaml

ML outlived the prover it was made for. In 1978 Milner proved that a program his type checker accepted could not “go wrong”, and the checker needed no annotations, because it inferred every type itself.²2Robin Milner, A Theory of Type Polymorphism in Programming, Journal of Computer and System Sciences 17, 1978. Roger Hindley had found the principal type independently, for combinatory logic, in 1969. His Turing Award named ML too, as “the first language to include polymorphic type inference together with a type-safe exception-handling mechanism”.³3The ACM Turing Award citation, 1991, as given in Robin Milner 1934–2010, POPL 2011.

At INRIA, Gérard Huet’s team took ML in its own direction and released Caml in 1987. Xavier Leroy rewrote it as Caml Light in 1990, gave it a native compiler and a module system in 1995, and with Didier Rémy and Jérôme Vouillon’s objects it became Objective Caml in 1996, OCaml for short, in which one program can be functional, imperative and object-oriented at once.⁴4A History of OCaml, ocaml.org.

People started building with it things that had to be right. In 2003 Astrée, an analyser written in OCaml at the École normale supérieure, proved that the primary flight control software of the Airbus A340, 132,000 lines of C, could never stop on a run-time error, and Airbus took it on for the A380.⁵5The Astrée Static Analyzer, École normale supérieure. Jane Street, the trading firm that would grow into Wall Street’s leading market maker, began writing its systems in OCaml in the early 2000s.⁶6Jane Street Capital, in Philip Wadler’s list of functional programming in the real world. Facebook wrote the type checkers for Hack and Flow in it, and Infer, which checks every change to its mobile apps before it ships.⁷7Hack: a new programming language for HHVM, March 2014, Flow, a new static type checker for JavaScript, November 2014, and Open-sourcing Facebook Infer, June 2015, Engineering at Meta. Fun fact, the first Rust compiler was written in OCaml too, until Rust could compile itself in 2011,⁸8Bootstrapping the compiler, the rustc-dev-guide. and so is the reference interpreter of WebAssembly.⁹9The WebAssembly reference interpreter.

What grew around the language took a different path. Its community came mostly from universities, research labs and companies where guarantees mattered more than anything else, and each built the tools it needed. For years OCaml had two standard libraries, several build systems, a few quite different ways to compile to JavaScript, and two concurrency libraries incompatible with each other, which left “a split OCaml world with almost no interoperability, and duplication of efforts”, as one of their users put it in 2014.¹⁰10Rudi Grinberg, Abandoning Async, December 2014. The second standard library is Jane Street’s Base. The language was ready long before its ecosystem, and for years the ecosystem was what people judged it by.

Meanwhile the language kept moving. Until version 5, OCaml, like many other languages at the time, was multi-threaded but single-core, because its runtime, garbage collector included, “was really designed with sequential executions in mind”.¹¹11Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026.

Making a runtime truly parallel is hard in itself. The garbage collector has to keep working while many threads change memory at once, and stay fast, since the easy way out, a lock around every operation on memory, would make a program “run as slowly as on a single processor”.¹²12Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026. The language also needs a memory model that says what a program may see when two threads touch the same data, every choice trading speed against simplicity.¹³13Stephen Dolan, KC Sivaramakrishnan and Anil Madhavapeddy, Bounding Data Races in Space and Time, PLDI 2018.

Doing it to a mature language is harder still, because the millions of lines already written must keep working, and keep their speed.¹⁴14KC Sivaramakrishnan and others, Retrofitting Parallelism onto OCaml, ICFP 2020. The OCaml team, most of it at OCaml Labs in Cambridge, spent more than eight years on it. OCaml 5 came out in December 2022 with parallelism across cores and algebraic effects.¹⁵15OCaml 5.0.0 is out, 16 December 2022.

What is a type

All of that rests on the one thing Milner put in first, the type, and the word is used loosely enough to need pinning down before anything leans on it.

The idea is older than computers. Bertrand Russell sketched a theory of types in 1903 and set it out in 1908, to keep mathematics out of its paradoxes by sorting things into kinds that cannot be mixed, and in 1940 Alonzo Church gave it the form programming languages later borrowed.¹⁶16Thierry Coquand, Type Theory, the Stanford Encyclopedia of Philosophy. A type in a program does the same job. It says what kind of thing a value is, and so what can be done with it.

Every program makes assumptions about its data. This value is a number, that list is never empty, a payment is in one of four states. A type writes such an assumption down where a machine can check it. A language without types still has the assumptions, keeps them in the programmer’s head, and finds out one was wrong when the program runs, in front of whoever is using it. That works while the person who made the assumptions is the one changing the code. It stops working when the code is large, or old, or changed by someone who was never told, and that describes most code an agent touches.

Types can do that job in two ways. A type can describe a value or bind it. A binding type is one the program cannot break, whatever code anyone writes, the way a binding contract is one you cannot walk away from when it gets inconvenient. A describing type is the program’s own account of itself, and nothing makes it true.

The two languages most of us write are Python and TypeScript.¹⁷17Stack Overflow Developer Survey 2025, technology. In both, the types came afterwards, written on top of a language that runs without them.

JavaScript was made in 1995 so that anyone could write a few lines straight into a web page,¹⁸18Allen Wirfs-Brock and Brendan Eich, JavaScript: The First 20 Years, HOPL IV, 2020. and for years those lines mostly made text scroll and snow fall. Then it grew into the language of every web application, with nothing to hold one together. TypeScript is the most successful attempt to fix that. It is JavaScript with types written in, and its compiler checks them and then strips them out, so what runs is plain JavaScript that knows nothing of them. To work with whatever JavaScript was already there, its design goals promise to “preserve runtime behavior of all JavaScript code” and keep the types “fully erasable”, and they list a sound type system among the non-goals.¹⁹19TypeScript Design Goals, goals 7 and 9, and non-goal 3. So every type can be opted out of, and the way out is any. A value of type any can be called, assigned and read from as anything, and whatever is read from it is any too,²⁰20Everyday Types, the TypeScript Handbook. so one any spreads quietly through every value it touches. JSON.parse returns one, and this compiles without a word:

function chargeCard(customerId: string, amount: number) { ... }

const shipping = 5;
const order = JSON.parse(body);        // any
const total = order.total + shipping;  // any too, and the API sent "49.90"
chargeCard(order.customerId, total);   // accepted as a number, charges "49.905"

A TypeScript codebase is as strict as its least careful line, and at worst it is JavaScript with annotations.

Python was never about types. Guido van Rossum started it in December 1989 as a hobby project for the Christmas week,²¹21Guido van Rossum, Foreword for “Programming Python”, 1996. and it grew up as a language for prototypes, scripts and science long before anyone asked it to hold a large system together. Types arrived in 2014 as hints, with the promise that “Python will remain a dynamically typed language, and the authors have no desire to ever make type hints mandatory, even by convention”.²²22PEP 484 – Type Hints, 2014. What checking there is lives in separate tools, mypy and pyright, each with its own rules, and only if somebody runs them.

A type that describes is advice, and an agent takes advice the way it takes instructions. A type that binds is a check, and a check cannot be ignored.

What the compiler refuses

Now OCaml. Take a payment. It is pending, paid, refunded or disputed, and each state carries only what belongs to it:

type payment =
  | Pending
  | Paid of { amount : int; receipt : string }
  | Refunded of { amount : int; reason : string }
  | Disputed of { amount : int; case_id : string }

Only a paid payment has a receipt, and there is no way to write a refund without its reason. Disputes came last, and somebody forgot the one function that decides whether a payment can be refunded:

let can_refund = function
  | Paid _ -> true
  | Pending | Refunded _ -> false

Warning 8 [partial-match]: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: Disputed _

The compiler finds the function nobody opened and names the case it misses. It reports it as a warning, and Dune, OCaml’s build tool, turns the warning into an error in development builds,²³23Dune’s build profiles. so nothing builds until every such function has been handled. TypeScript catches it only in a switch whose author remembered to add a workaround for it, Python only when a separate checker runs in strict mode, and Go has no such types at all.²⁴24Exhaustiveness checking, the TypeScript Handbook, Unreachable code and exhaustiveness checking, Python’s typing documentation, and Why does Go not have variant types?, the Go FAQ.

There is no null either. Tony Hoare added the null reference to ALGOL W in 1965, “simply because it was so easy to implement”, and later called it his billion-dollar mistake.²⁵25Tony Hoare, Null References: The Billion Dollar Mistake, QCon London, 2009. Java still pays it on every reference. Go pays it twice, since an interface holding a nil pointer is not itself nil, and its FAQ has a whole entry on why “my nil error value” is not equal to nil.²⁶26Why is my nil error value not equal to nil?, the Go FAQ. In OCaml a user is always a user, and a user who might not be there is a user option, which the compiler makes you open before you touch it.

Effects

A program spends much of its life waiting, for a database, the network, a disk. The simplest way to wait is to block, to stop the thread until the answer comes, and most web frameworks did just that for years, one thread per request, which holds up until there are more requests than threads a machine can afford. The other way is an event loop, one thread that never waits and juggles thousands of requests, starting each piece of I/⁠O and coming back to it when it is done.

async and await are how TypeScript, Python and Rust let ordinary-looking code run on that loop. They tell the compiler where a function may pause and hand the thread back to the loop, and they do nothing else, so one blocking call inside an async function still stalls everything else on it. And the marks spread. Bob Nystrom called it in 2015 “the colour of a function”, because an async function can only be awaited from another async one.²⁷27Bob Nystrom, What Color is Your Function?, 2015. Here is a greeting built on a lookup that reads from memory:

function findUser(id: number): User { ... }

function greet(id: number): string {
  return `Hello, ${findUser(id).name}`;
}

function welcome(id: number): string {
  return `<h1>${greet(id)}</h1>`;
}

The lookup moves to a database and becomes async, and greet stops compiling, because what comes back is no longer a user:

Property 'name' does not exist on type 'Promise<User>'.

So greet becomes async, then welcome, then whatever calls welcome, all the way up:

async function findUser(id: number): Promise<User> { ... }

async function greet(id: number): Promise<string> {
  return `Hello, ${(await findUser(id)).name}`;
}

async function welcome(id: number): Promise<string> {
  return `<h1>${await greet(id)}</h1>`;
}

One function started waiting and three changed. Libraries split the same way, one kind for code that waits and one for code that doesn’t, and in Rust it runs deep enough that its language team opened an initiative in 2022 to let one function be both.²⁸28Announcing the Keyword Generics Initiative, Inside Rust, July 2022.

OCaml 5 has a different answer, from programming language research, called algebraic effects.²⁹29Gordon Plotkin and Matija Pretnar, Handlers of Algebraic Effects, ESOP 2009. A function can perform an effect, a request it does not answer itself, and a handler somewhere up the stack answers it and resumes the function exactly where it stopped, like an exception that can come back with a value:

(* Declare an effect: a question whose answer is a string. *)
type _ Effect.t += Ask_name : string Effect.t

(* greet asks the question and carries on with the answer. *)
let greet () = "Hello, " ^ Effect.perform Ask_name

let () =
  match greet () with
  (* greet finished: print what it returned. *)
  | greeting -> print_endline greeting
  (* greet asked for a name: k is the rest of greet, paused there.
     Resume it with the answer. *)
  | effect Ask_name, k -> Effect.Deep.continue k "Robin"

greet asks for a name without knowing who answers. Here the handler answers “Robin”. A test could answer with a fixture, and a scheduler could answer “not yet”, put greet aside, run something else, and come back once the name arrives from a database. Generators, coroutines, lightweight threads and async itself can all be built this way, as libraries, with nothing marked in between.³⁰30KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer and Anil Madhavapeddy, Retrofitting Effect Handlers onto OCaml, PLDI 2021.

That one mechanism does more than end the colours. Code asks, and the handler around it decides, so what other languages need a dependency injection framework for comes close to being a property of the language. And a paused function keeps a real stack of its own, so the debuggers and profilers that walk the stack keep working on code that waits.³¹31The same paper: the implementation “remains compatible with program analysis tools that inspect the stack”.

TypeScript has an ambitious library after the same idea, Effect, where a program is a value of type Effect<Success, Error, Requirements>, “a description of a workflow or operation that is lazily executed”, which tracks in its types the errors and dependencies OCaml leaves untyped.³²32The Effect Type, Effect’s documentation. It is a library on top of the language, though, so the code that uses it is written as Effect values, in generators or pipelines, and calling it from plain TypeScript is a boundary of its own, another colour. OCaml has effects in the language itself, so a function that uses one is written like any other function, and the functions that call it do not change.

Eio is the library that puts effects to work for I/⁠O and concurrency in OCaml 5.³³33Eio, effects-based direct-style I/⁠O for OCaml 5. It sets a waiting function aside and runs others until its answer arrives, so the lookup can move to a database and greet does not change by a character:

let greet db id = "Hello, " ^ (Users.find db id).name

and running two lookups at once is a function call, not a new kind of function:

let profile db id =
  let user, orders =
    Eio.Fiber.pair
      (fun () -> Users.find db id)
      (fun () -> Orders.recent db id)
  in
  { user; orders }

For an agent it is the difference between a change and a cascade. Making one function talk to the network touches that one function in OCaml, and in a coloured language it touches every caller up to main, in files the agent was never asked to open. OCaml is one of very few languages with effects built in, and the research behind them is still moving.³⁴34On typed effects, which the compiler would check: Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley and Anton Lorenzen, Modal Effect Types, OOPSLA 2025.

What the others traded

Rust stands apart, and for good reason. It was made to solve the memory safety problem, and it solves it.³⁵35Why Rust?, rust-lang.org: its “rich type system and ownership model guarantee memory-safety and thread-safety”, “with no runtime or garbage collector”. The price is an ownership model the engineer works out and the compiler enforces, who owns each value, who may borrow it and for how long. Leroy calls it “the finest language that I know for manual memory management”, and that is its trade, since “it’s significantly harder to write programs when you have to manage your memory”.³⁶36Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026. It shows in the code. Here is a cache of users in Rust:

fn remember(cache: &Rc<RefCell<HashMap<u64, Rc<User>>>>, user: User) -> Rc<User> {
    let user = Rc::new(user);
    cache.borrow_mut().insert(user.id, Rc::clone(&user));
    user
}

The same in OCaml:

let remember cache user =
  Hashtbl.replace cache user.id user;
  user

Every word Rust adds is about memory, and none of it is about users. An agent writing Rust spends its effort, and the compiler its refusals, on the machinery rather than on the domain. Rust’s own survey found that 55% of those who answered wait more than ten seconds for an incremental rebuild of their slowest project, and compile times were among the reasons given by 45% of those who stopped using it.³⁷37Rust compiler performance survey 2025 results, September 2025. An agent works in a loop, a change and the compiler’s feedback, many times over, and the OCaml compiler keeps that loop short. What it builds is predictable too, so you know before it runs what will be fast and what will be slow.³⁸38Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026.

Every one of them traded something away. OCaml is the one that did not, and it reads like what it means. Every module has its contract in an interface file, every state is named in a type, so nobody has to read the code, and anybody can.

Who bet on it

The biggest bet is Jane Street’s. Its people made it “the world’s largest industrial user of the language”,³⁹39Yaron Minsky’s biography in Real World OCaml. with more than thirty million lines of OCaml written by over five hundred people,⁴⁰40Large Scale Trading System, ocaml.org. and Reuters reported a record $39.6 billion of net trading revenue for it in 2025, calling it “Wall Street’s leading market maker”.⁴¹41Anirban Sen, Jane Street’s $40 billion trading haul tops rivals, sources say, Reuters, April 2026. What it wants from OCaml is speed, reliability and code that people who are not programmers can read, “like financial engineers or quantitative analysts”.⁴²42Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026. It gives back in kind. Jane Street is a platinum sponsor of the OCaml Software Foundation,⁴³43The OCaml Software Foundation, its sponsors. funds work on the compiler,⁴⁴442020 at OCamlPro, on Flambda, built with Jane Street. and Yaron Minsky, who brought OCaml there and heads its technology group, co-wrote Real World OCaml, the book on using it in production, which anyone can read online.⁴⁵45Yaron Minsky and Anil Madhavapeddy, Real World OCaml, second edition, Cambridge University Press, 2022.

Bloomberg built BuckleScript, a compiler from OCaml to JavaScript, in 2016,⁴⁶46OCaml compiler brings type safety to JavaScript, InfoWorld, September 2016. and Melange carried it on inside the OCaml world when BuckleScript became ReScript.⁴⁷47Melange’s rationale, melange.re. Ahrefs, the SEO company, crawls the whole web every day with OCaml on more than four thousand servers,⁴⁸48Petabyte-Scale Web Crawling and Data Processing, ocaml.org, and OCaml Developer, Ahrefs careers. and in 2023 it moved all of its front ends to Melange as well.⁴⁹49Ahrefs is now built with Melange, Ahrefs tech blog, May 2023. MirageOS builds unikernels in OCaml, each an operating system made of only the libraries one application needs, and Docker’s networking on Mac and Windows came from it.⁵⁰50MirageOS, and Anil Madhavapeddy, Improving Docker with Unikernels, Docker blog, May 2016. Owl, begun at the University of Cambridge in 2016, does scientific and engineering computing in OCaml.⁵¹51Owl, a system for scientific and engineering computing in OCaml.

The objection that matters for agents is that models have read far less OCaml than TypeScript or Python, and Jane Street trains its own for that reason.⁵²52John Crepezzi, Building AI-Powered Developer Tools at Jane Street, AI Engineer Summit, 2025. Leroy’s latest feedback is that the OCaml models write is “quite decent and quite similar in quality to more popular languages”, and that “one thing that seems to help the generative AI is a type system”.⁵³53Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026. Where a model does get it wrong, the compiler tells it so on its first try. In a language that describes, the same mistake gets through and waits for a user to find it.

Writing code gets cheaper, and checking that it is correct does not.⁵⁴54Xavier Leroy, Creator of OCaml: Functional Programming, Formal Verification, Programming Languages, interviewed by Ryan Peterman, July 2026. A type checker is the cheapest check there is.

One language to rule them all

OCaml’s problem was never a lack of libraries so much as libraries that fit together. A library that made its own choices about errors, JSON or time makes every one around it translate. A coherent ecosystem is what matters, and it is why Jane Street built its own, with its own standard library, its own concurrency and its own build tool, which became Dune, the one most OCaml projects build with.⁵⁵55Core, Jane Street’s standard library overlay, Async, and Dune 1.0.0, which began at Jane Street as Jbuilder.

OCaml 5 adds a second problem to the first. Effects are new, so most OCaml libraries were written before them and do not use them. Eio could only exist once OCaml 5 did. An ecosystem that uses OCaml 5 in full has to be built for it.

And we build one — Hypha Stack, components made to fit together. Spindle serves the API over HTTP, wiretype describes its data once, rowtype and postgres-eio put that data in Postgres, spool runs the jobs, and solidtype builds the UI, to name a few.

Look at how little it takes. A line of an order, as wiretype’s own example has it:

type line = {
  sku : string;
  quantity : int; [@min 1] [@max 99]
  note : string option; [@max_length 200]
} [@@deriving wiretype]

From these five lines come a type the compiler holds every use of, a check on every request that reports every problem at once,

quantity: This must be at most 99. (too_large)
note: This must be text, not a number. (unexpected_type)

the API’s OpenAPI document, and the same type in the front end, through a client printed from the server’s routes on every build.

So the server and the front end cannot disagree about what a line is. A change on the server that the front end has not caught up with is a compile error, found by whoever made the change, seconds after making it, with its file and line. In a stack that finds out at run time the same change ships, a user meets it as a broken page, and someone works back from there to the cause. SQL gets the same treatment, since rowtype checks every statement against the migrated database before anything ships.

The same holds above the code. We are building an ontology of what a backend is made of — each concept, what it means, which component provides it, which checks hold it — and it is written in OCaml too.

Milner did not trust the person at the computer at night, himself included, and he did not ask them to be more careful. He built a language in which the careless thing could not be written. An agent will stay up all night writing code, and it should, in a language that says no.