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

> Source: <https://anil.recoil.org/notes/ocaml-modules-agentic>
> Published: 2026-10-09 00:00:00+00:00

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!)