I've been doing a fair bit of agentic OxCaml programming in the past year, and consistently finding that OCaml is a perfect fit across the spectrum of languages 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,
then exercise them with a test client,
then fill in the implementations.
After that we get more exotic and refine with OxCaml modes
and finish by speculating where formal proofs could go.
1 First build up only the module interfaces
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 may be helpful.
(* 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.
(* 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.
$ dune build @check
This interface compiles without warnings, so it's time to exercise our fledgling interface with a test binary!
2 Building a test client for this interface
By writing a binary next, we can test if the interface we just defined is sufficiently precise to actually use externally.
(* 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:
$ 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"
We therefore edit our interface to add the constructor function:
(* 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!
$ 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
3 Fill in the module implemenations one at a time
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, which keep the expected output next to the code).
(* 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:
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.
3.1 Stopping agents from taking shortcuts
A tempting shortcut for an agent in Book is to treat money as a plain integer and do
the operations directly within that implementation:
(* 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.
(* 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!
$ 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.
4 Refining even more with OxCaml modes
We don't have to stop at just OCaml interfaces though! OxCaml is a language extension from Jane Street that provides mode annotations that can extend this workflow. (If you want to learn more, we ran an OxCaml tutorial at ICFP 2025.)
We can now run an agentic pass to refine our interfaces to have even more checks:
(* 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.
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. (I run these agents in a sandboxed devcontainer.) Crucially, these mode annotations helped to stop an agent introducing a subtle error that may have corrupted data when used across multiple processsors.
5 Going deeper down the refinment rabbithole
All the OxCaml modes earliy are statically defined by the compiler, which is getting increasingly capable. The ICFP 2026 mode crossings 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 in the interfaces?!
Here's a sketch of Money using a Gospel-style specification. 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 that had these features (PLDI 2008 paper). I'm really excited that it's heading back into modern OxCaml as I've been jealous of Liquid Haskell 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 and our own work on 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!)