Linux Foundation Launches New Organization To Maintain TLA+ (techcrunch.com) 16
The Linux Foundation, 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. From a report: 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.
To give a few examples, ElasticSearch, the organization behind the search engine of the same name, used TLA+ to verify the correctness of their distributed systems algorithms. Elsewhere, Thales, the electrical systems manufacturing firm, used TLA+ to model and develop fault-tolerant modules for its industrial control platform. "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."
To give a few examples, ElasticSearch, the organization behind the search engine of the same name, used TLA+ to verify the correctness of their distributed systems algorithms. Elsewhere, Thales, the electrical systems manufacturing firm, used TLA+ to model and develop fault-tolerant modules for its industrial control platform. "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."
Re: (Score:2)
News For Nerds, But Not Math Nerds!
Huge corporations (Score:2)
Huge corporations love this stuff, and yeah it's a snooze fest.
I don't get "programming languages" that don't produce the working executable. Presumably there's still a human in the loop looking at all this, but if you've got 10s of thousands of employees what's another 100 to look over something like this, and they say it actually found bugs so there's that.
It's just that it's so far beyond the realm of the 1 to 5 person development that got so many of us to be inspired and creative. At the opposite end
Re: (Score:2)
Huge corporations love this stuff, and yeah it's a snooze fest.
It's the first I'd heard about it and I thought it was pretty fascinating.
I don't get "programming languages" that don't produce the working executable.
As far as I can tell, it's only the bozos at TechCrunch that are calling it a programming language. Its homepage [azurewebsites.net] just refers to it as a language. Kinda like how HTML is a language, but not a programming language.
Thanks but... (Score:2)
nope.
I'd prefer if they finish for once the (dead) LaTeX 3 spec and implementation (now called LaTeX 2.e-what-ever-I-don't-remember-now-because-why-to-use-a-different-number-for-a-different-spec-when-you-can-drive-crazy-users?-Ha-ha-ha).
It's real? (Score:4, Funny)
How can someone come up with "TLA" as an acronym and it doesn't stand for "Three Letter Acronym"
Yes, It's real? (Score:2)
TLA = "Temporal Logic of Actions". It uses a mathematical notation. TLA+ [wikipedia.org] is a formal language for TLA.
ETLA (Score:2)
However, "TLA+" does not qualify. Instead, it's an ETLA: "extended three-letter acronym."
Re: (Score:2)
> it's an ETLA: "extended three-letter acronym."
So, a four-letter word.
So now Linux will be funding... (Score:2)
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
Looks to me this is a way for Corporations to pull funds from the Linux Foundation. So now they can hire people and say the are working on a TLA+, bonuses all around.
Or another take, they donate to the Foundation, get a tax cut, then pull funds for "TLA+ development". Laundering anyone ???
Will a poor unemployed person get a piece of the pie ? We know the answer to that.
Another ivory tower language nobody asked for (Score:1)
What is the TLA+ programming language, you ask?
No, I did not ask.
It's a formal "spec" language developed by computer scientist and mathematician Leslie Lamport. Best known for his seminal work in distributed systems
Despite decades in IT industry and science and on all kinds of news channels, the only context I have heard Lamport's name in is that of LaTeX authorship. His "notable papers" (according to his Wikipedia page) were published at a time when we had implemented and deployed lots of "distributed systems" already, so no, that work was not "seminal".
Lamport -- now a scientist at Microsoft Research
Ah, so it is just another Microsoft advertisement in disguise, or an attempt of theirs to distract others from competing with what really makes them
Re: (Score:2)
His "notable papers" (according to his Wikipedia page) were published at a time when we had implemented and deployed lots of "distributed systems" already, so no, that work was not "seminal".
He won a Turing award for his work. You have no idea what you are talking about.
Re: (Score:2)
No, this is not an MS advertisement.
Since TFA and TFS apparently did such a bad job at conveying what TLA+ is, I'll summarize it here:
TLA+ is a language plus set of tools that enable analysis of concurrent state machines. Imagine a program that relies on three concurrent threads of execution that each modify some shared state in a complex manner. Analy
"What is the TLA+ programming language, you ask? " (Score:2)
No one asked. It's self-referential vaporware.