One-pager (pitch) why companies would want to join our foundation #3
Conversation
@pressron initial version
There was a problem hiding this comment.
I have added a few small comments. The main question for me is who is the target audience of this text. This seems to be introductory text selling TLA+ to somebody who has never used it. Are we expecting this text to be read by the leadership of the companies who have invested into learning it and using it (e.g., Amazon, Microsoft)? If so, we need at least one paragraph about why the foundation, language and tools need financial support. The tools are there and it is not immediately clear, what the foundation would do about them. There are only two closing sentences that talk about the future.
|
|
||
| TLA+ is particularly attractive for industry use compared to other formal methods. Its unique strengths in specifying concurrent and distributed systems make it applicable precisely where mainstream software needs help the most. It can specify arbitrary properties of systems of arbitrary complexity and "ordinary" developers can still learn it in a few weeks. Automated verification with a model checker makes the cost of verification low enough to compare favorably with traditional assurance methods. | ||
|
|
||
| For those reasons, TLA+ is among the most popular formal methods in industry, employed successfully by Amazon, Oracle, Microsoft, ElasticSearch, MongoDB, and others. This [technical report from Amazon](http://lamport.azurewebsites.net/tla/amazon-excerpt.html) relates how engineers learned TLA+ in just a few week. They then found and fixed potentially catastrophic and hard-to-reproduce problems in several AWS services. |
There was a problem hiding this comment.
The Amazon paper was published in Communications of ACM too: https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext
|
|
||
| TLA+ is particularly attractive for industry use compared to other formal methods. Its unique strengths in specifying concurrent and distributed systems make it applicable precisely where mainstream software needs help the most. It can specify arbitrary properties of systems of arbitrary complexity and "ordinary" developers can still learn it in a few weeks. Automated verification with a model checker makes the cost of verification low enough to compare favorably with traditional assurance methods. | ||
|
|
||
| For those reasons, TLA+ is among the most popular formal methods in industry, employed successfully by Amazon, Oracle, Microsoft, ElasticSearch, MongoDB, and others. This [technical report from Amazon](http://lamport.azurewebsites.net/tla/amazon-excerpt.html) relates how engineers learned TLA+ in just a few week. They then found and fixed potentially catastrophic and hard-to-reproduce problems in several AWS services. |
There was a problem hiding this comment.
| For those reasons, TLA+ is among the most popular formal methods in industry, employed successfully by Amazon, Oracle, Microsoft, ElasticSearch, MongoDB, and others. This [technical report from Amazon](http://lamport.azurewebsites.net/tla/amazon-excerpt.html) relates how engineers learned TLA+ in just a few week. They then found and fixed potentially catastrophic and hard-to-reproduce problems in several AWS services. | |
| For those reasons, TLA+ is among the most popular formal methods in industry, employed successfully by Amazon, Oracle, Microsoft, ElasticSearch, MongoDB, CrowdStrike, Informal Systems, and others. This [technical report from Amazon](http://lamport.azurewebsites.net/tla/amazon-excerpt.html) relates how engineers learned TLA+ in just a few week. They then found and fixed potentially catastrophic and hard-to-reproduce problems in several AWS services. |
There was a problem hiding this comment.
CrowdStrike -- sure. But we should only specifically list companies worth over $1B and have a Wikipedia entry (or, at least, are so famous that everyone has heard of).
There was a problem hiding this comment.
I thought you wanted to have a proof of TLA+ being used in industry. I only have seen TLA+ specs publicly available from Microsoft, ElasticSearch, MongoDB, and Informal Systems. Amazon's specs are hidden under NDA. Oracle? Never seen anything.
Do we all agree about this criterion: But we should only specifically list companies worth over $1B and have a Wikipedia entry (or, at least, are so famous that everyone has heard of)?
There was a problem hiding this comment.
Most companies won't open-source their TLA+ specs. For example, the only spec ever published by Microsoft was specifically written to be public user documentation. All other specifications are confidential.
To keep the paragraph short, why don't we lobby our peers to have their employers/companies added to https://github.com/tlaplus/awesome-tlaplus#users and link to it here? If say, an Oracle employee, created the PR that added Oracle to https://github.com/tlaplus/awesome-tlaplus#users, I'd assume this to be good enough to convince execs.
There was a problem hiding this comment.
My questions here are "what do we want this to accomplish, and how?" As it stands this is a piece hyping up TLA+ and why we want to develop it further. If we're trying to convince companies to join our foundation, we need to talk about the benefits they'd get for joining.
|
|
||
| Turing Award-winner Leslie Lamport invented TLA+ in the '90s as the culmination of decades of research in concurrent and distributed systems. It has gained a measure of popularity in the industry since the 2010s, as distributed systems started growing in size and use, and it's become clear that traditional quality assurance methods fail to catch some of the costliest bugs. | ||
|
|
||
| As Lamport is nearing retirement from Microsoft Research, he wishes to entrust TLA+ to a foundation to ensure TLA+'s relevance and growth are supported by donations of funds and personnel. The foundation will also invest in promising avenues to make TLA+ easier to use or more powerful, such as tools that monitor if a production system deviates from its specification at runtime. Another avenue are tools that could generate tests from the specifications. |
There was a problem hiding this comment.
This is the only part that talks about why companies would want to join the foundation, as opposed to use (or appreciate) TLA+. This covers the benefits to us if they join; what about the benefits to them if they join?
There was a problem hiding this comment.
You're right. My thinking here was that once an executive is convinced that TLA+ is useful and should survive (and evolve), they will then be interested in the precise contribution levels and benefits, which could be the subject of another document. But if there's something short and powerful we could add here -- we should. I don't know what it is, though.
|
|
||
| ### Where TLA+ Has Been and Where It's Going | ||
|
|
||
| Turing Award-winner Leslie Lamport invented TLA+ in the '90s as the culmination of decades of research in concurrent and distributed systems. It has gained a measure of popularity in the industry since the 2010s, as distributed systems started growing in size and use, and it's become clear that traditional quality assurance methods fail to catch some of the costliest bugs. |
There was a problem hiding this comment.
Are we going all in on saying "this is a tool for distributed systems"? Do we want people to think that they should use other tools if they don't have a concurrent system?
There was a problem hiding this comment.
Because the main pain-point vis-à-vis correctness and its cost that established companies face is distributed systems, I believe this is where TLA+ gives the most bang for the buck for the intended audience. I could add something about other kinds of systems, but we need to keep an eye out for the length.
|
This is an executive summary targeted at executives. At least two companies (Oracle and Mongo) asked for one. Because of that, there is a pretty strict length limit. It should be something that an executive can read in under two minutes, so about 500 words. |
Please add links to papers that support our claim that TLA+ provides real value for "ordinary" (software) engineering.
Initially created by @pron.