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.

---

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

• We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
• We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
• We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
• We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.