linux-code-binary-100938204-orig.jpg?auto=webp=85,70
TLA+ (Temporal Logic of Actions), a programming language for modeling programs and systems, particularly concurrent and distributed ones, is moving from Microsoft’s jurisdiction to the Linux Foundation and getting its own, separate foundation to promote it.
The TLA+ Foundation, an independent non-profit organization dedicated to fostering the adoption and development of the language, was launched by the Linux Foundation on April 21. The TLA+ Foundation will provide education and training, fund research, develop tools, and build a community of practitioners. Inaugural members of the TLA+ Foundation include Oracle, Microsoft, and Amazon Web Services (AWS).
The TLA+ language has been used to verify complex software systems, reduce errors and improve reliability, the Linux Foundation said. The language purports to detect design flaws early in the development process to save resources and time.
Underpinning TLA+ is the notion that the best way to describe things precisely is with simple mathematics. TLA+ and its tools, according to the Linux Foundation, are useful for eliminating fundamental design errors that are hard to find and expensive to correct in code. The language was invented by computer scientist Leslie Lamport, now a distinguished scientist with Microsoft Research.
Among the users of TLA+ is Oracle, which has used the language to model more than 25 services of Oracle Cloud Infrastructure, including the block storage and file storage services, and verify the correctness of complex design scenarios including distributed replication, failover, and live re-sharding.
