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."
Related Stories
Bryan Lunduke has gone over the 2023 Linux Foundation report. He has observed that the foundation spends even less on the kernel than ever, both in absolute dollars and in percentage of the budget. It spends around 2% on Linux and 98% on everything else.
While it's true that The Linux Foundation continues to grow substantially -- now bringing in over a quarter of a Billion dollars per year (seriously) -- the total amount spent on the Linux kernel dropped roughly $400,000 in 2023. (Not surprising as The Lunduke Journal previously pointed out that lowering the total support of Linux appeared to be the goal.)
- The percentage of The Linux Foundation revenue spent on Linux dropped in 2023.
- And the total amount spent dropped as well.
- All while funding of non-Linux projects (such as AI and Blockchain) continued to dominate.
As many notice, budget aside, the foundation does not advance or promote the kernel, rather the opposite. It represents its members' corporate interests inside kernel development. Bruce Perens pointed out about six years ago that the membership the basically amounts to a GPL infringers club.
Previously:
(2023) Linux Foundation Launches New Organization to Maintain TLA+
(2021) Linux Foundation and Partners Announce "Open 3D Foundation"
(2021) Linux Foundation Unveils Sigstore
(2020) Linux Foundation Does Not Eat its Own Dogfood
(Score: 2) by bart9h on Tuesday April 25 2023, @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 2023, @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 2023, @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 2023, @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.
Impeach Donald Saruman and his sidekick Elon Sauron
(Score: 2) by JoeMerchant on Wednesday April 26 2023, @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.
🌻🌻🌻 [google.com]
(Score: 2) by mcgrew on Saturday April 29 2023, @06:21PM (1 child)
Big < > formal, little < > informal.
Impeach Donald Saruman and his sidekick Elon Sauron
(Score: 2) by JoeMerchant on Sunday April 30 2023, @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.
🌻🌻🌻 [google.com]
(Score: 2) by turgid on Saturday May 20 2023, @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 2023, @11:43PM
We should make sure they pledge to not be evil here.
(Score: 2) by Gaaark on Wednesday April 26 2023, @12:56AM
Yeah: there goes the neighborhood.
--- Please remind me if I haven't been civil to you: I'm channeling MDC. I have always been here. ---Gaaark 2.0 --
(Score: 2) by jb on Wednesday April 26 2023, @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 2023, @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!
Impeach Donald Saruman and his sidekick Elon Sauron
(Score: 0) by Anonymous Coward on Wednesday April 26 2023, @03:12PM
(Score: 1) by deganee on Thursday April 27 2023, @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 2023, @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.
I am not interested in knowing who people are or where they live. My interest starts and stops at our servers.