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.
[...] With the establishment of the TLA+ Foundation, the Linux Foundation says it'll provide education and training resources around TLA+, fund research and develop tools for it and work to foster a community of TLA+ practitioners. The TLA+ Foundation will also make decisions on language enhancements, address user feedback and guide the language's evolution.
"TLA+ has already been successfully used by major tech companies like Amazon, Oracle, and Microsoft to verify and design planetary-scale systems," the spokesperson continued. "By establishing a TLA+ Foundation under the umbrella of the Linux Foundation, TLA+ will gain increased visibility and support, promoting its wider adoption within the tech industry. The foundation's mission to advocate for open-source projects will ensure that TLA+ continues to evolve and remain accessible to the broader tech community. Additionally, the foundation will facilitate greater collaboration between industry and academia, advancing the state of the art in formal methods and concurrent and distributed systems research."
(Score: 2) by bart9h on Tuesday April 25, @10:52PM (9 children)
A formal specification language would be great. If that succeeds, we will probably want an AI bot to translate TLA+ to actual code in an actual programming language of your preference.
(Score: 4, Interesting) by HiThere on Tuesday April 25, @11:08PM (8 children)
It's backed by Amazon, Oracle, and Microsoft.
I'd be really careful about thinking this is a good idea.
Javascript is what you use to allow unknown third parties to run software you have no idea about on your computer.
(Score: 5, Insightful) by Rosco P. Coltrane on Tuesday April 25, @11:22PM (5 children)
Just because something was made or backed by an unsavory person or organization doesn't automatically make that thing bad. The Nazis were against smoking and invented the autobahn for example. And Googles comes with brilliant computer products and tools all the time despite being one of the most disgusting and most nefarious member of the corporate surveillance industry.
(Score: 2) by mcgrew on Wednesday April 26, @01:44PM (3 children)
One, sure, I'll agree, but when Satan, Beezlebub, Baal, and the devil all back something, it's wise to note that just maybe it's not the best thing that could happen.
I would not trust any plan cooked up by a consortium made of James Buchanan, Richard Nixon, and Donald Trump, for example. I would disregard it out of hand, even if saying tobacco was bad was part of it.
Carbon, The only element in the known universe to ever gain sentience
(Score: 2) by JoeMerchant on Wednesday April 26, @09:45PM (2 children)
It could also be because these organizations are at a scale where they need this kind of formalism to prevent their projects from spiraling into chaos and failure so much of the time.
The fact that they are so big is what puts them in the company of Baal et. al., something about a rich man, heaven, camel and the eye of a needle...
Even smaller organizations can benefit from the formalism that larger organizations are hurt so badly by not exercising. Once your organization grows beyond the one programmer and a couple of sales guys scale, the benefits of formalism start growing.
Україна досі не є частиною Росії Слава Україні🌻 https://news.stanford.edu/2023/02/17/will-russia-ukraine-war-end
(Score: 2) by mcgrew on Saturday April 29, @06:21PM (1 child)
Big < > formal, little < > informal.
Carbon, The only element in the known universe to ever gain sentience
(Score: 2) by JoeMerchant on Sunday April 30, @12:28AM
In my experience, anything more than about 2.5 software engineers and you start to benefit from some formal methods. I was at a place with 8 programmers and almost no formalism, it was a non-stop comedy of errors.
Україна досі не є частиною Росії Слава Україні🌻 https://news.stanford.edu/2023/02/17/will-russia-ukraine-war-end
(Score: 2) by turgid on Saturday May 20, @09:21AM
What with they use it for themselves, though?
I refuse to engage in a battle of wits with an unarmed opponent [wikipedia.org].
(Score: 0) by Anonymous Coward on Tuesday April 25, @11:43PM
We should make sure they pledge to not be evil here.
(Score: 2) by Gaaark on Wednesday April 26, @12:56AM
Yeah: there goes the neighborhood.
--- Please remind me if I haven't been civil to you: I'm channeling MDC. ---Gaaark 2.0 ---
(Score: 2) by jb on Wednesday April 26, @06:36AM
Interesting. I would have thought Lamport was *best* known for his work on LaTeX.
(Score: 3, Insightful) by mcgrew on Wednesday April 26, @01:38PM (1 child)
What does TLA stand for? Most names are descriptive, acronyms are not. Do none of you remember clueless middle managers talking about "the doss", referring to DOS and having no clue what an operating system was or that DOS stood for Disk Operating System?
If you're explaining a concept, NEVER use an acronym, or at least say WTF that SA (Stupid Acronym) stands for!
Carbon, The only element in the known universe to ever gain sentience
(Score: 0) by Anonymous Coward on Wednesday April 26, @03:12PM
(Score: 1) by deganee on Thursday April 27, @03:25AM (1 child)
Does the Linux kernel use TLA+? I'm stupid. Why does Linux (or anyone) care about this. Are there any examples where someone has used TLA+ in a useful, practical, large project?
(Score: 2) by janrinok on Thursday April 27, @11:50AM
Why should you care? It could affect anyone who writes software professionally. Not today maybe, but the Linux Foundation seems to believe it might in the future.