The TLA+ programming language is moving from Microsoft to Linux, getting its own, separate foundation to promote it, InfoWorld reports.
TLA+ is a high-level language for modeling programs and systems, especially concurrent and distributed ones. TLA+ has been used successfully by companies to verify complex software systems, reducing errors and improving reliability. The language helps to detect design flaws early in the development process, which in turn saves time and resources.
TLA+ and its tools are useful for debugging basic design errors that are difficult to find and correct in code. The language is based on the idea that the best way to accurately describe things is using simple mathematics.
“As the world’s reliance on distributed systems grows, it’s important for developers to have TLA+’s capabilities to formally model and verify systems behave as they were intended.”
said Jim Zemlin, executive director at the Linux Foundation.
The language was invented decades ago by computer science pioneer Leslie Lamport, who is now a distinguished scientist at Microsoft Research. After many years of leadership by Lamport and support from Microsoft, TLA+ is now part of the Linux Foundation.
The TLA+ Foundation will promote adoption, provide education and training resources, fund research, develop tools, and build a community of TLA+ practitioners. The TLA+ Foundation’s role as the language committee will ensure the continuous improvement and evolution of the TLA+ language. The TLA+ Foundation will make decisions on language enhancements, address user feedback and needs, maintain high safety and reliability standards, and guide the language’s evolution to better serve its user base.
By joining the TLA+ Foundation, we aim to support the advancement of TLA+ tooling and further improve the state of the art in distributed systems design,”
said Byron Cook, Vice President and Distinguished Scientist at AWS.
More big tech companies are becoming part of this foundation.
“We are excited to join TLA+ Foundation as a founding member with the goal of furthering the TLA+ toolkit and improving the quality of distributed cloud services in the years to come,”
said Pradeep Vincent, SVP and OCI Chief Technical Architect, Oracle.
“The TLA+ Foundation is timely in so many ways. Thinking systemically and analytically about software development is more needed now than ever. The complexity of often-networks software systems is going up and we need tools like TLA+ to cope,”
said Vint Cerf, Vice President and Chief Internet Evangelist at Google.
NVIDIA didn’t stand idly by either.
“NVIDIA actively uses formal methods in the development of safety/security critical software and hardware, including TLA+, which we use to formalize our designs and requirements. The TLA+ foundation fulfills another important need; promoting the wider use of formal methods in industry to improve product quality; especially where safety and security are critical,”
said Tom McReynolds, Senior Director DRIVE OS SW, NVIDIA.
The TLA+ Foundation invites technology companies to join it and support its mission to promote the development of TLA+ in the software industry. The mission of the TLA+ Foundation is to be able to continue to improve the capabilities of this language and to help ensure that the benefits of TLA+ are available to all, which is exactly why the Foundation is inviting companies to join.