As software engineers, we're always on the lookout for tools and technologies that can enhance our ability to create robust, reliable software. The recent "Lean FRO Year 1 in Review" report by Leonardo de Moura, Sebastian Ullrich, and Corinna Calhoun (2024) highlights some developments in the world of formal methods that are particularly relevant to our field. Let's dive into the key takeaways from the first year of the Lean Focused Research Organization (Lean FRO) and explore how they might impact software engineering.

Advancements in Software Verification

One of the most significant developments for software engineers is Lean's contribution to hardware and software verification. The report mentions that AWS has integrated Lean with Cedar "to achieve software verification at the highest level of correctness". This integration, along with the use of SampCert in AWS Clean Rooms Differential Privacy service, demonstrates the growing adoption of formal methods in commercial software development.

Improved Proof Automation

Lean has made strides in proof automation, which is crucial for practical application of formal methods in software engineering. These advancements can potentially make formal verification more accessible and efficient for software engineers.

Package Management and Build Tools

Software engineers will appreciate Lean's focus on developer tools. The launch of Reservoir, Lean's package repository, and its integration with Lake, the Lean build tool, mirrors the package management systems we're familiar with in software development. This infrastructure can facilitate easier adoption and use of Lean in software projects.

For instance, you can find SATurn, a SAT solver-prover in Lean, at Reservoir. SATurn is based on the DPLL algorithm. As Siddhartha Gadgil, the author of SATurn wrote, "Given a SAT problem, we get either a solution or a resolution tree showing why there is no solution."

Performance and Scalability Improvements

The report highlights "key architectural changes to make Lean faster, simpler, and more robust". These improvements, including the upstreaming of a large part of the standard library, are crucial for the practical application of formal methods in large-scale software projects.

Open Source Development Model

With 406 closed issues on GitHub, 1545 merged PRs, and over 900 improvements implemented, Lean demonstrates a vibrant open-source ecosystem. This model of development is familiar to many software engineers and can provide opportunities for community involvement and contribution.

Documentation

The creation of Verso, a tool for producing high-quality Lean documentation, addresses a critical need in software engineering. For instance, The Lean Project Blog is implemented using Verso. "With Verso, each post is itself a Lean file."

Lean FRO team members

Lean FRO hired eleven Lean FRO team members. One of them is Sofia Rodrigues, which I interviewed in my Elixir em Foco podcast (in Portuguese)!

Learning Resources

If you want to learn more about Lean as a programming language, I suggest the free e-book Functional Programming in Lean, by David Thrane Christiansen.

Conclusion

Lean FRO's progress in its first year shows promising advancements in formal methods that are increasingly relevant to software engineering. From improvements in software verification and proof automation to the development of supporting tools and resources, Lean is making strides towards making formal methods more accessible and practical for everyday software development.

As software engineers, we should keep an eye on these developments. While formal methods may still seem daunting, tools like Lean are bridging the gap between theoretical correctness and practical application. As the field evolves, incorporating formal methods into our toolkit could significantly enhance our ability to create reliable, verifiable software systems.