Why Lean 4 replaced OCaml as my Primary Language
10 days ago
- #OCaml
- #programming_languages
- #Lean
- The author transitioned from OCaml to Lean as their primary programming language due to several pain points with OCaml.
- OCaml's philosophy of WYSIWYG (What You See Is What You Get) leads to predictable but manual performance optimizations, requiring developers to balance readability and performance.
- OCaml's conservative and slow release cycle ensures stability but delays the introduction of new features, such as dynamic arrays, which took years to be added to the standard library.
- OCaml's metaprogramming capabilities are limited and complex, with macros (ppx) being syntax-to-syntax transformations without type information or hygiene guarantees.
- Lean offers advanced metaprogramming features, including extensible syntax and type-aware macros, making it more flexible and powerful for developers.
- OCaml's build system, Dune, is opinionated and works well for standard projects but can be restrictive for custom or complex build processes.
- Lean's build system, Lake, is written in Lean itself, offering greater flexibility and extensibility for custom build processes.
- The author highlights that OCaml's features are beneficial for companies prioritizing stability, while Lean is more suited for developers seeking cutting-edge language features and flexibility.