The TLA+ Foundation has been launched with the aim of bringing math-based software modeling to the mainstream. The TLA+ Foundation is part of the Linux Foundation, with Microsoft, Amazon Web Services (AWS), and Oracle serving as founding members. 

TLA+ is a high level, open-source, math-based language for modeling computer programs and systems, especially concurrent and distributed ones. The language has tools to help eliminate fundamental design errors and the new foundation aims:

"to help further refine the tools and spur commercial usage and additional research".

The Linux Foundation said that the TLA+ Foundation will promote adoption, provide education and training resources, fund research, develop tools, and build a community of TLA+ practitioners.

The TLA language was first published in 1993 by computer scientist Leslie Lamport, now, at age 82 a distinguished scientist with Microsoft Research. Lamport also invented the document preparation system LaTeX and won the 2013 Turing Award for his work to clarify distributed systems. 

TLA stands for Temporal Logic of Actions, and it's based on the idea that you can build systems more effectively by using algorithmic models to specify how the code should work, in the same was as an engineer would create blueprints to guide the construction of a bridge. TLA+ comes with a model checker that will check whether satisfying a program's specification implies that the code will do what it should. Lamport explained that:

"When programmers write systems, they should start by defining what they are supposed to do and check that their work will do it. That's a better way than just sitting down to write the code, based on some vague outline."

The foundation says that TLA+ has already been adopted for industrial use by semiconductor makers, companies that build distributed and database systems, other tech companies, and in more mainstream applications like payment systems in retail stores. The hope is that the foundation's role in setting up a formal system for contributing to the tools and defining their future direction will result in additional collaboration among engineers and in greater commercial adoption. The foundation will create a steering committee, similar to other panels that look after public domain programming languages like C or Java.

Lamport said that:

"TLA+ is never going to be as popular as Java. And I'd be happy if someone else made it better at helping engineers think more mathematically. The ultimate goal is to get engineers to think rigorously at a higher level about what they are doing."

The TLA+ Foundation is now up and running. 

More Information

TLA+ Foundation Website

TLA+ Foundation On GitHub

The TLA+ Home Page

Related Articles

Leslie Lamport On Programming As More Than Coding

Leslie Lamport Wins Turing Award