Linux Foundation Launches New Organization to Maintain TLA+

upstart writes:

Linux Foundation launches new organization to maintain TLA+:

The LinuxFoundation, 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.

[...] "TLA+ is unique in that it's intended for specifying a system, rather than for implementing software," a Linux Foundation spokesperson told TechCrunch via email. "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.

Read more of this story at SoylentNews.