Why Lean 4 replaced OCaml as my Primary Language

Issue number 1 is one of the reasons Xavier Leroy cited for OCaml’s success

What made that possible? Not just fancy types and nice modules – even though systems programmers value type safety and modularity highly – but also basic properties of OCaml:

  • a language with a simple cost model, where it’s easy to track how much time and how much space is used;

  • a compiler that produces efficient code that looks like the source code, with only predictable optimizations;

  • a low-latency garbage collector, usable for soft real-time applications.

    To us PL folks, this doesn’t sound like much. Good luck getting a paper accepted at POPL or PLDI based on these ideas! Yet, that’s crucial to open the way to many exciting applications.

11 Likes