[Meta] Specify the TLA+ enhancement process

[lemmy]

What should the TLA+ enhancement process look like?

• What kind of change "requires" an RFC (where do bugs stop)?
• How to include the voices of the community at large?
• Who gets to vote?
• How is related work organized and tracked that potentially spans multiple organizations/companies?
• Do we want to and, if yes, how to unite research- and engineering-focused efforts (research doesn't want to be scooped)?
• ...

Goals

• Foster wider adoption of TLA+ (the idea of high-level specs) in industry and education
• Provide a way for the community to express their support for enhancements
• Consistency of the TLA+ ecosystem
• Guarantee "vendor neutrality"
• Inclusiveness
• Foster research
• ...

TODO

• Lay out rules of engagement => code of conduct

[lemmy]

The repository name should change from RFCs to something that better communicates that this is also about bigger enhancements still in the requirements phase? It also has to be made clear that proposers cannot expect others to do the work; proposing an enhancement ideally creates synergies, but the proposer is the driver.

[konnov]

Shall we add "foster wide industry adoption" to the goals?

[ligurio]

I'm not about process, but anyway. It may be worth to create an issue template with recommended fields and parts of RFC.
GH allows to create it, see https://docs.github.com/en/communities/using-templates-to-encourage-useful-issues-and-pull-requests/configuring-issue-templates-for-your-repository

[lemmy]

@ligurio Great idea, do you know of a popular/matching template we could re-use?

[ligurio]

I would start with at least following sections:

• summary with short description of proposal
• proposal itself
• a list of things in scope and out of scope
• motivation and use cases
• benefits
• drawbacks

I hope it would enough for start.

P.S. see also RFC templates in reactjs project, tensorflow and rust-lang.

Update: GH discussions can be used for discussing RFCs, we found it very convenient in our project.

[lemmy]

The Technical Charter provides scaffolding: https://foundation.tlapl.us/docs/TLA%2B%20Project%20Technical%20Charter.pdf

[ahelwer]

Here is the prototype which was (is being?) mostly followed by the unicode RFC, not from any grand plan but because each step seemed like the most reasonable at the time:

1. Open a RFC for the given issue here; provide a statement of the problem, motivation for solving it using the standardization process, and summary of how current tools handle the proposal and what changes will be necessary to bring the RFC to completion.
2. Identify a RFC champion - probably, the person who opened the RFC - who is being relied upon to push the RFC from proposal to adoption to completion. While the champion is not personally responsible for implementing every aspect of the RFC, they should remain an active participant in the TLA+ community until the RFC is fully ratified by the tools.*
3. The champion should bring up the RFC for discussion at one or more community meetings (depending on scope - larger changes should entail greater discussion), to build awareness and consensus among longstanding community members.
4. If there aren't any strong objections, the champion or associate should implement a proof of concept in some subset the TLA+ tools. If consensus continues to hold and the proof of concept is brought to production-ready state with associated thorough testing, the changes should be merged into the tools. It is not required that all tools be brought to conformance before the initial merge; incremental development is acceptable.
5. A directory should be created in the tlaplus-standard repo to track RFC ratification among the TLA+ tools maintained by the TLA+ Foundation.
6. The champion or their associates should endeavor to continue pushing the tools to full ratification of the RFC.

*There is considerable ambiguity here as to what "fully ratified" means in the context of software engineering, where bugs and additional associated work are inevitable after any substantial changes. RFCs abandoned by the champion partway through implementation can face reversion if the added workload is considered more trouble than it's worth by remaining contributors; however, if the feature has seen uptake from the community then users should be consulted before reversion.

[lemmy]

The proposal above does not mention the Specification Language Committee (SLC), which, as outlined in the Technical Charter, is responsible for overseeing and ratifying the evolution of TLA and TLA+, while seeking input from the community at large. This model is at odds especially with regards to the last sentence, which implies de facto standards.

[ahelwer]

We do currently have de facto standards (whatever the Java tools do). I definitely support efforts to create a unified standard independent of any given implementation. I hadn't heard of the SLC before but presumably their approval would be required.