OCaml's module language is the perfect fit for agentic programming

Anil Madhavapeddy argues that OCaml's module language, with its separation of .mli interface files from .ml implementations, is a strong fit for agentic programming because coding agents fill well-specified holes better than they handle million-line codebases. In a worked example, he defines a Money module and a Book module as interfaces only, compiles them with the dune directive (modules_without_implementation money book), then writes a test client that fails with 'Error: Unbound value "Money.of_pence"' because the interface was too abstract to construct a Money.t, prompting him to add val of_pence : int -> t option. The post extends the approach to OxCaml modes and speculates about formal proofs.

I've been doing a fair bit of agentic OxCaml programming https://anil.recoil.org/notes/cresting-the-ocaml-ai-hump in the past year, and consistently finding that OCaml is a perfect fit https://anil.recoil.org/notes/cresting-the-ocaml-ai-hump across the spectrum of languages https://anil.recoil.org/notes/life-zarr-and-everything I've been developing in recently. If you're not familiar with OCaml, this post is a quick guide as to why I think this. As codebases get larger, a coding agent is better at filling in a 'well-specified hole' than cramming in a million-line codebase into its context window. OCaml has a clean separation between .mli files an interface definition for a module and the .ml implementations. I'll follow with with a toy project that has two modules, but the technique scales to million-line codebases. We'll start by writing only the interfaces https://anil.recoil.org/ first-build-up-only-the-module-interfaces , then exercise them with a test client https://anil.recoil.org/ building-a-test-client-for-this-interface , then fill in the implementations https://anil.recoil.org/ fill-in-the-module-implemenations-one-at-a-time . After that we get more exotic and refine with OxCaml modes https://anil.recoil.org/ refining-even-more-with-oxcaml-modes and finish by speculating where formal proofs could go https://anil.recoil.org/ going-deeper-down-the-refinment-rabbithole . We have a module Money that tracks our cash i.e it shoudl never be negative . If you need help with the syntax then the RWO guided tour https://dev.realworldocaml.org/guided-tour.html may be helpful. php lib/money.mli type t val add : t - t - t val sub : t - t - t option sub a b is None if b a . val to string : t - string to string m is e.g. "£3.05" . The Book module is a list of deposits and withdrawals. php lib/book.mli type t val empty : t val deposit : Money.t - t - t val withdraw : Money.t - t - t, Insufficient of Money.t result Insufficient bal carries the balance that was too small. val balance : t - Money.t Notice that we don't have any implementations yet, but that the types we have defined can reference each other's module despite this. This OCaml project can be made to compile via a dune directive to suppress the need for an implementation as well. library name ledger modules without implementation money book Now the magic begins, as we can typecheck our project from just this descrption of how they should work together. bash $ dune build @check This interface compiles without warnings, so it's time to exercise our fledgling interface with a test binary By writing a binary next, we can test if the interface we just defined is sufficiently precise to actually use externally. js bin/main.ml open Ledger let = let let = Option.bind in let r = let ten = Money.of pence 1000 in let three = Money.of pence 305 in let b = Book.deposit ten Book.empty in match Book.withdraw three b with | Ok b - Some Money.to string Book.balance b | Error - None in print endline Option.value r ~default:"failed" The first realisation when we compile it is that our interface was too abstract, so we have no way to make a Money.t This makes the build fail: bash $ dune build @check File "bin/main.ml", line 5, characters 15-29: 5 | let ten = Money.of pence 1000 in ^^^^^^^^^^^^^^ Error: Unbound value "Money.of pence" The interface we first designed was too abstract, and nothing outside Money can produce a value of its type. So now we can edit our interface and add the constructor functions: php lib/money.mli type t val of pence : int - t option of pence n is None if n < 0 . Now the binary typechecks, and fails at linking time complaining that there's no implementation. But because the type checker has passed it, we know that the interface is good enough to be worth implementing bash $ dune build ./bin/main.exe Error: No implementations provided for the following modules: "Ledger Money" referenced from bin/.main.eobjs/native/dune exe Main.cmx "Ledger Book" referenced from bin/.main.eobjs/native/dune exe Main.cmx We can now hand Money to the coding agent with an instruction to read the interface .mli files, and start implementing the module implementations in dependency order with tests per module such as expect tests https://blog.janestreet.com/testing-with-expectations/ , which keep the expected output next to the code . js lib/money.ml type t = int let of pence n = if n < 0 then None else Some n let add = + let sub a b = if b a then None else Some a - b let to string m = Printf.sprintf "£%d.%02d" m / 100 m mod 100 The dune link error now only complains about Ledger Book . The agent then moves onto writing the Book module, with similar instructions to only read the interface files. This then brings up another problem with the interface, as writing Book.empty shows needs a starting balance. At this point the agent uses its context-driven discretion to either use of pence , or add a helper function to Money : js File "lib/book.ml", line 3, characters 12-22: 3 | let empty = Money.zero ^^^^^^^^^^ Error: Unbound value "Money.zero" If the user or agent goal agrees to reassess the interface design, the Book interface gains a zero function. A tempting shortcut for an agent in Book is to treat money as a plain integer and do the operations directly within that implementation: js lib/book.ml type t = Money.t let empty = Money.zero let deposit m b = Money.add m b let withdraw m b = if m b then Error Insufficient b else Ok b - m let balance b = b This results in a type error in OCaml though: Error: The implementation "lib/book.ml" does not match the interface "lib/.ledger.objs/byte/ledger Book.cmi": Values do not match: val withdraw : int - int - int, Insufficient of int result is not included in val withdraw : t - t - t, Insufficient of t result Type "int" is not compatible with type "t" The agent can't subtract pence directly, since the OCaml interfaces enforce that only the Money module can perform this operation over a value of that type. Conveniently, the compiler rejects it with a message that's helpful enough for the agent to write the correct implementation from the Money interface. js lib/book.ml type t = Money.t let empty = Money.zero let deposit m b = Money.add m b let withdraw m b = match Money.sub b m with | Some b' - Ok b' | None - Error Insufficient b let balance b = b This now fully builds end-to-end, yay bash $ dune build ./bin/main.exe && ./ build/default/bin/main.exe £6.95 The great thing about this technique is that it scales to enormous projects with hundreds of mli files, and this agentic workflows allows for a cheap definition of a complex set of interfaces before embarking on the expensive implementations. OCaml's separate compilation keeps build times very fast so we have a quick edit/compile loop. We don't have to stop at just OCaml interfaces though OxCaml https://oxcaml.org is a language extension from Jane Street that provides mode annotations https://doi.org/10.1145/3674642 that can extend this workflow. If you want to learn more, we ran an OxCaml tutorial https://anil.recoil.org/notes/icfp25-oxcaml at ICFP 2025. We can now run an agentic pass to refine our interfaces to have even more checks: php lib/money.mli type t : immutable data val add : t @ local - t @ local - t val to string : t @ local - string lib/book.mli type t : immutable data The immutable data annotations promises that a Money.t or Book.t contains no mutable state in its implementation, so it can e.g. be shared freely between parallel threads. The @ local ensures that a function doesn't hold onto its argument, so the caller can pass in a stack-allocated value and not have to have heap allocations https://anil.recoil.org/notes/oxcaml-httpz . An agent that decides to "optimise" Book with a mutable balance now fails: type t = { mutable bal : Money.t } Error: The implementation "lib/book.ml" does not match the interface "lib/.ledger.objs/byte/ledger Book.cmi": Type declarations do not match: type t = { mutable bal : Money.t; } is not included in type t : immutable data The kind of the first is mutable data with Money/2.t @@ forkable unyielding many because of the definition of t at file "lib/book.ml", line 1, characters 0-34. But the kind of the first must be a subkind of immutable data. The first mode-crosses less than the second along: contention: mod uncontended ≰ mod contended visibility: mod read write ≰ mod immutable This error is admittedly a little opaque to a human user something that's being worked on in OxCaml , but it's fine for an agent with an OxCaml skill https://github.com/avsm/ocaml-claude-marketplace/blob/main/plugins/ocaml-dev/skills/oxcaml/SKILL.md . I run these agents in a sandboxed devcontainer https://anil.recoil.org/notes/ocaml-claude-dev . Crucially, these mode annotations helped to stop an agent introducing a subtle error that may have corrupted data when used across multiple processsors. All the OxCaml modes earliy are statically defined by the compiler, which is getting increasingly capable. The ICFP 2026 mode crossings https://people.mpi-sws.org/~bpeters/papers/mode-crossing.pdf paper this summer shows how the compiler automatically strengthens modes for values of certain types, which is how our Money.t can declare immutable data succinctly. But wouldn't it be cool if we could also express arbitrary logical conditions https://x.com/JulesJacobs5/status/2108144426640175371 in the interfaces? Here's a sketch of Money using a Gospel-style specification https://github.com/ocaml-gospel/gospel . I've not actually compiled this one, but you'll get the idea: lib/money.mli type t @ model pence : integer invariant pence = 0 val sub : t - t - t option @ r = sub a b ensures match r with | None - a.pence < b.pence | Some c - c.pence = a.pence - b.pence The comment is now a machine-checked contract, so every implementation must guarantee it satisfies these pre- and post-conditions. About two decades ago, Patrick Rondon and Ranjit Jhala worked on a liquid OCaml https://github.com/ucsd-progsys/dsolve that had these features PLDI 2008 paper https://patrickrondon.com/research/papers/liquid-types-pldi08.pdf . I'm really excited that it's heading https://x.com/JulesJacobs5/status/2108144426640175371 back into modern OxCaml as I've been jealous of Liquid Haskell https://ucsd-progsys.github.io/liquidhaskell/ for a long time :- The beautiful thing about using OCaml's module system as a basis for these formal extensions is that separate compilation architecture I sketched above means that the edit/feedback loop is fast even on million-line codebases. The layering of annotations also lets us make code progressively more specified without piling on huge numbers of unit tests. This is context efficient for agents and preserves human sanity as code gets more complex. We're also only beginning to investigate how to visualise such constraints in our user interfaces, like the work ongoing in Hazel https://hazel.org and our own work on bidirectional type slicing https://anil.recoil.org/papers/2026-bidirectional-type-slicing to debug type errors also this last paper just got conditionally accepted into POPL 2027, which I'm super excited about and will wrote more on later