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 technewss via ema. “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, faures in software design are surprisingly common — and disruptive. A 2020 report from the Standish Group found that around 66% of software projects fa. And according to the Consortium for Information and Software Quality, poor software quality cost companies over $2 trlion 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 wl also make decisions on language enhancements, address user feedback and guide the language’s evolution.
Secure your spot at TC Sessions: AI and show 1,200+ decision-makers what you've but — without the big spend. Avaable through May 9 or whe tables last.
“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+ wl gain increased visibity and support, promoting its wider adoption within the tech industry. The foundation’s mission to advocate for open-source projects wl ensure that TLA+ continues to evolve and remain accessible to the broader tech community. Additionally, the foundation wl facitate greater collaboration between industry and academia, advancing the state of the art in formal methods and concurrent and distributed systems research.”