The Linux Foundation, the nonprofit tech consortium that manages various open source efforts, today announced the launch of the TLA+ Foundation to promote the adoption and development of the TLA+ programming language. AWS, Oracle and Microsoft are among the inaugural members.
What is the TLA+ programming language, you ask? It’s a formal “spec” language developed by computer scientist and mathematician Leslie Lamport. Best known for his seminal work in distributed systems, Lamport — now a scientist at Microsoft Research — created TLA+ to design, model, document and verify software programs — particularly those of the concurrent and distributed variety.
To give a few examples, ElasticSearch, the organization behind the search engine of the same name, used TLA+ to verify the correctness of their distributed systems algorithms. Elsewhere, Thales, the electrical systems manufacturing firm, used TLA+ to model and develop fault-tolerant modules for its industrial control platform.
“TLA+ is unique in that it’s intended for specifying a system, rather than for implementing software,” a Linux Foundation spokesperson told TechCrunch via email. “Based on mathematical concepts, notably set theory and temporal logic, TLA+ allows for the expression of a system’s desired correctness properties in a formal and rigorous manner.”
TLA+ includes a model checker and theorem prover to verify if a system’s specification satisfies its desired properties. The goal is to assist developers with reasoning about systems above the code level, uncovering and preventing design flaws (hopefully) before they evolve into bugs during the later stages of software engineering.
To that last point, failures in software design are surprisingly common — and disruptive. A 2020 report from the Standish Group found that around 66% of software projects fail. And according to the Consortium for Information and Software Quality, poor software quality cost companies over $2 trillion in 2020.
With the establishment of the TLA+ Foundation, the Linux Foundation says it’ll provide education and training resources around TLA+, fund research and develop tools for it and work to foster a community of TLA+ practitioners. The TLA+ Foundation will also make decisions on language enhancements, address user feedback and guide the language’s evolution.
“TLA+ has already been successfully used by major tech companies like Amazon, Oracle, and Microsoft to verify and design planetary-scale systems,” the spokesperson continued. “By establishing a TLA+ Foundation under the umbrella of the Linux Foundation, TLA+ will gain increased visibility and support, promoting its wider adoption within the tech industry. The foundation’s mission to advocate for open-source projects will ensure that TLA+ continues to evolve and remain accessible to the broader tech community. Additionally, the foundation will facilitate greater collaboration between industry and academia, advancing the state of the art in formal methods and concurrent and distributed systems research.”
