Lean 4: When Sound Programs become a Choice

---

Monitoring Edge Technical Endeavours

As a company specialized in strongly-typed programming languages with strong static guarantees, OCamlPro closely monitors the ongoing trend of bringing more and more of these elements into mainstream programming languages. Rust is a relatively recent example of this trend; another one is the very recent Lean 4 language.

Lean 4, the Promising Future of Proven Software

Lean 4 builds on the shoulders of giants like the Coq proof assistant, and languages such as OCaml and Haskell, to put programmers in a world where they can write elegant programs, express their specification with the full power of modern logics, and prove that these programs are correct with respect to their specification. Doing all this in the same language is crucial as it can streamline the certification process: once Lean 4 is trusted (audits, certification...), then programs, specifications, and proofs are also trusted. This contrasts with having a programming language, a specification language, and a separate verification/certification tool, and then having to argue about the trustworthiness of each of them, and that the glue linking all of them together makes sense. This is extremely interesting in the context of critical embedded systems in particular, and in qualified/certified "high-trust" development in general.

While admittedly not as mainstream as Rust, Lean 4 has recently seen an explosion in interest from the media, developers, mathematicians, and (some) industrials. Quanta now routinely publishes articles about/mentioning Lean 4; Fields medalist Terry Tao is increasingly vocal about (and productive with) its use of Lean 4, see here and here for (very technical) example(s). On the industrial side, Leonardo de Moura (Lean 4's lead designer) recently went from a position at Microsoft Research to Amazon Web Service, which was followed by a fast and still ongoing expansion of the infrastructure around Lean 4.

Pushing for a Future of Trustworthy Software

OCamlPro has been closely monitoring Lean 4's progress by regularly developing in-house prototypes in Lean 4. Getting involved in the community and Lean 4's development effort is also part of our culture. This is to give back to the community, but also to closely follow the evolution of Lean 4 and sharpen our skills.

There are a few notable and public examples of our involvement. As part of our in-house prototyping, we discovered a "major bug" in Lean 4's dependent pattern-matching; later, we contributed on improving aspects of the by notation (used to construct proofs), which then ricocheted into fixing problems into the calc tactic. More recently, we contributed on various fronts such as improving the ecosystem's ergonomics, adding useful lemmas to Lean 4's standard library, contributing to the documentation effort...

Lean 4 is not of industrial-strength yet, but it gets closer and closer. Quickly enough for us to think that now's a reasonable time to spend some time exploring it.

---

Au sujet d'OCamlPro :

OCamlPro développe des applications à haute valeur ajoutée depuis plus de 10 ans, en utilisant les langages les plus avancés, tels que OCaml et Rust, visant aussi bien rapidité de développement que robustesse, et en ciblant les domaines les plus exigeants (méthodes formelles, cybersécurité, systèmes distribués/blockchain, conception de DSLs). Fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique) que pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (OCaml, Rust, Cobol, Python, Scilab, C/C++, etc.) et appliquée à de multiples domaines. Nous dispensons également des [formations sur mesure certifiées Qualiopi sur OCaml, Rust, et les méthodes formelles] (https://training.ocamlpro.com/) Pour nous contacter : contact@ocamlpro.com.