According to the Linux Foundation, the TLA+ Foundation has been established to encourage the acceptance and advancement of the TLA+ programming language. This nonprofit tech group coordinates several open-source initiatives. Microsoft, Oracle, and AWS are a few of the founding members.
You might wonder what the TLA+ programming language is. A computer scientist, and mathematician, Leslie Lamport, created it as a formal “spec” language. Lamport, a scientist at Microsoft Research and well-recognized for his groundbreaking work in distributed systems, developed TLA+ to design, model, describe, and verify software programs, particularly those that are concurrent and distributed.
To confirm the accuracy of their distributed systems algorithms, ElasticSearch, the company behind the search engine of the same name, used TLA+. TLA+ was also utilized by Thales, a manufacturer of electrical systems, to model and create fault-tolerant modules for its industrial control platform.
A Linux Foundation representative emailed TechCrunch, saying, “TLA+ is unique in that it’s intended for specifying a system rather than building software. TLA+ enables the formal and rigorous representation of a system’s desired correctness properties. It is based on mathematical ideas, particularly set theory and temporal logic.
To determine whether a system’s specification satisfies its required attributes, TLA+ comes with a model checker and theorem prover. The objective is to help programmers think about systems at a higher level than the code level, finding and avoiding design defects (ideally) before they grow into issues during the later stages of software engineering.
Regarding the last issue, it’s shocking how frequently and disruptively software design errors occur. A 2020 Standish Group analysis shows that 66% of software projects fail. Furthermore, the Consortium for Information and Software Quality estimates that in 2020, businesses would have lost more than $2 trillion due to subpar software.
The Linux Foundation states that creating the TLA+ Foundation will support research into and provide tools for TLA+, as well as endeavor to create a community of TLA+ practitioners. The TLA+ Foundation will also decide on language improvements, consider user comments, and direct the language’s development.
The representative added that major IT firms like Amazon, Oracle, and Microsoft have already used TLA+ to verify and design planetary-scale systems. “By establishing a TLA+ Foundation under the auspices of the Linux Foundation, TLA+ will receive more attention and support, encouraging a wider adoption within the tech sector. The foundation’s goal of supporting open-source initiatives will guarantee that TLA+ keeps developing and is available to the larger IT community. The foundation will also encourage increased industry-academia cooperation, improving the field of formal techniques and research on concurrent and distributed systems.
