Why Lean 4 replaced OCaml as my Primary Language

An important aspect of OCaml that newcomers might want to bear in mind is that it is a language and community that prides themselves on being "unsurprising", and this reflects in a philosophy of WYSIWY.

The key guiding principle across OCaml code is that it is very easy to reason about, and a seasoned OCaml dev can quickly tell you exactly how a given OCaml function behaves at runtime, its performance and how it allocates memory, etc.

let List.iter f =
    function
    | [] -> ()                     (* no alloc *) 
    | h :: t -> f h; List.iter f t (* no alloc *)

let sum ls =
    let sum = { contents = 0 } in  (* alloc (1 block) *)
    let f x = sum := !sum + x in   (* alloc (closure) *) 
    List.iter f ls;                (* no alloc *)
    a.contents                     (* no alloc *)

For example, just by looking at the above block of code, we can instantly tell that it allocates one block of memory and one closure on the heap.

This simplified model means that the runtime performance of code is very predictable, and it's easy to manually optimise code, but…

This means as a developer you alone are entirely responsible for making your code go fast, and sometimes this can mean obscuring the logic of your program in the quest for performance.

As a slightly more concrete example, consider the following function, to calculate the both the sum of a list and increment each value by its index:

let incr_sum ls =
  let f = (fun (sum, i) vl ->   (* alloc (closure) *)
      let sum = sum + vl in
      let vl = vl + i in
      let acc = (sum, i + 1) in (* alloc (tuple) *)
      (vl, acc)                 (* alloc (tuple) *)
    )
  let (ls, (sum, _len)) ==
      List.fold_map ls (0,0) in (* alloc (list + tuple) *)
  (ls, sum)                     (* alloc (tuple) *)

I've written it out in an expanded form to make the allocations clear, but if I were really code-golfing, I'd probably write it in my own code in the following simplified form:

let incr_sum ls =
  let open Pair in
  let update vl =
    Fun.flip (map_same2 (+)) (vl, 1) &&& snd_map ((+) vl) in
  List.fold_map (Fun.flip update) (0,0) ls
  |> map_fst fst
  |> swap

Who said only Haskell programs could be unreadable⁴. Anyway, that being said, from a performance perspective, this implementation is not ideal because it allocates a lot (doubly so for my simplified version) with intermediate tuples and closures.

If memory were to become a constraint, then, as the OCaml compiler itself is very conservative in its optimisations⁵, we would be forced to come back to this function and manually rewrite it in order to get the desired allocation patterns, for example:

let incr_sum ls =
  let i = ref 0 in              (* alloc (block) *)
  let sum = ref 0 in            (* alloc (block) *)
  let f = (fun vl ->            (* alloc (closure) *)
      i := !i + 1;
      sum := !sum + vl;
      vl + (!i - 1)             (* no allocs in hot-path *)
    ) in
  let ls = List.map f ls in     (* alloc (list) *)
  (ls, !sum)                    (* alloc (tuple) *)

In this case, if you come from an imperative background, then maybe this version of the program looks "better" for you, but in larger functional programs, building up such functional pipelines leads to more idiomatic and shorter code and as such is quite ubiquitous if you are an experienced OCaml dev.

The main point I'm making here is that, from an individual developer's perspective, I'm forced to strike a compromise between concisely expressing my intent (i.e computing this fold over a list), and obtaining high performance. In a vacuum, these compromises might be okay, but they also come with a cost of an increased maintenance burden.

Comparison to Lean

def incr_sum (ls: List Int) : List Int × Int := Id.run $ do
  let mut sum := 0
  let mut res := #[]
  for (vl, i) in ls.zipIdx do
    sum := sum + 1
    res := res.push (vl + i)
  return (res.toList, sum)

Branching out from the conservative nature of the language itself, this same philosophy of being conservative and backwards-compatible extends in some sense to the compiler ecosystem of the language itself. OCaml is an amazingly stable langauge, and major kudos have to be given to the community for insisting on such high standards for the ecosystem:

You can almost bet that code from more than a decade ago will run on the latest OCaml compiler, with minimal changes, if at all.

While this is great for ensuring the utility of your code over time, a sad consequence of this is that the language evolves at a very slow pace, and this extends even to things such as the standard library.

Consider this thread of adding dynamic arrays – that is, an array datastructure with O(1) access and resizable allocation:

type 'a t                              (* dynamic array *)
val alloc: int -> 'a t                 (* alloc *)
val (.[]): 'a t -> int -> 'a           (* O(1) get *)
val (.[]<-): 'a t -> int -> 'a -> unit (* O(1) set *)
val push: 'a t -> 'a -> unit           (* realloc (if needed) *)

This was initially proposed back in 2019 (6 years ago !!), by a fresh-eyed newcomer to the community:

The PR very quickly succumbed to orthogonal discussions of naming and was eventually closed.

Three years later, another PR was created in a second attempt but also fared the same fate:

It was only last year, that this long saga was finally concluded, and dynamic arrays joined the stdlib:

Now, there were legitimate reasons for the level of caution and discussions that the community took to introduce even such a simple datastructure to the language: given its focus on backwards compatibility, any introduction to the standard library would likely continue to have to be maintained for the forseeable future, so it was critically important to move carefully here.

Again, to stress the point, OCaml's strong commitment to backwards comparability, is genuinely and truly one of the most impressive features of the language, but you can also imagine that as a developer interested in extending and exploring new abstractions for their langauge of choice, this can be a bit of a dampener.

Features such as modular implicits, an OCaml-specific variant of type-classes have been being discussed for several years now, and are unlikely to be deployed anytime in the near future:

Comparison to Lean

This is a relatively minor point, but it's caused me some pain in the past, so I figured it's worth mentioning.

OCaml's build systems have evolved a lot over the years, and it has taken some time to converge upon a robust and efficient solution that works for most people. Thanks to the folks at Jane Street, who developed the Dune build system, OCaml now has a really nice and consistent story w.r.t building.

Simply write a dune file, which uses a pretty uncontroversial and simple s-expression-based syntax to describe your project and its dependencies, and voila, your project can be built with minimal fuss~

(library
   (name lib)
   (deps ...))

…that is assuming you're not straying too far from the "happy path".

That is, dune works well for most OCaml projects, but, as a self-titled "opinionated build manager", deliberately provides a restricted set of possible build actions — if you want to do things like generating text as part of your build and so on and so forth, you'll very quickly find yourself running into walls.

Dune supports a number of extensions beyond pure OCaml, such as supporting Ctype-based projects with FFI, and C builds, and even some Rocq build support, but these extensions are all driven mostly by what Jane Street wants or uses, and straying too far from the beaten path will lead to pain.

Comparison to Lean

import Lake

open Lean Lake DSL

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

require betterfind from "./BetterFind"

package probability where

lean_lib BallsInBins where

With that I've reached the end of the biggest pain-points I've had with OCaml over my time with it. Hopefully, it's given you an alternative perspective on the language and some of its features that you might not like.

I think an arguable caveat to all of these criticisms is that in some sense, they're only a problem if you're a solo-developer — the WYSIWY nature of the language, the restrictive metaprogramming support, the constrained build system and runtime representations are all features that, if you're a company looking for stable and consistent code, are arguably positives. This would certainly explain the popularity of OCaml in companies like Jane Street and Ahrefs, where unexciting and boring code is a distinct positive (no-one wants to be the one to explain why you just lost a bajillion dollars because your macro had a typo).

That being said, if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl!

Plus, as an extra benefit, you might even end up contributing to state of the art mathematics research~