The Linux Foundationthe non-profit technology consortium that manages several 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 is a formal ‘spec’ language developed by computer scientist and mathematician Leslie Lamport. Best known for his pioneering 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 eponymous search engine, used TLA+ to verify the correctness of their distributed system algorithms. Elsewhere, electrical systems manufacturer Thales used TLA+ to model and develop fault-tolerant modules for its industrial control platform.
“TLA+ is unique in that it is for specifying a system, rather than deploying software,” a Linux Foundation spokesperson told AapkaDost via email. “Based on mathematical concepts, especially set theory and temporal logic, TLA+ allows the desired correctness properties of a system to be expressed in a formal and rigorous way.”
TLA+ includes a model checker and theorem prover to verify whether the specification of a system meets the desired properties. The goal is to help developers reason about systems above the code level, uncovering and (hopefully) preventing design flaws before they develop into bugs during the later stages of software engineering.
Up to that last point, software design errors are surprisingly common—and disruptive. A 2020 report from the Standish Group found that about 66% of software projects fail. And according to the Consortium for Information and Software Quality, poor software quality will cost companies more than $2 trillion by 2020.
With the creation of the TLA+ Foundation, the Linux Foundation says it will provide education and training resources around TLA+, fund research and tools for it, and work to foster a community of TLA+ practitioners. The TLA+ Foundation will also make decisions about language improvements, answer user feedback, and guide the evolution of the language.
“TLA+ has already been successfully used by major technology companies such as Amazon, Oracle and Microsoft to verify and design planetary-scale systems,” the spokesperson continued. “Establishing a TLA+ Foundation under the umbrella of the Linux Foundation will give TLA+ greater visibility and support, furthering 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 wider technical community. In addition, the foundation will enable greater collaboration between industry and academia, advancing the state of the art in formal methods and research on concurrent and distributed systems.”