Update RFC process (rust-lang#2716)

I would like to incorporate a few suggestions to the RFC process and template:
  1. Suggest that the first RFC revision should not include implementation details. Thanks @feliperodri for the suggestion. 
  2. Change the template to (hopefully) clarify what should go in each section. @JustusAdam any suggestions?
  3. Change the template to clarify that open questions and future work should be simple lists.
  4. Replace `--enable-unstable` by `-Z` flag.

The main goal is to try to speed up the process by reducing the scope of the RFC document, breaking it down into multiple steps, and even reduce the need for an RFC entirely.

Co-authored-by: Felipe R. Monteiro <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Adrian Palacios <[email protected]>

Author: 4 people

rfc/src/intro.md

@@ -8,10 +8,10 @@ integrate feedback from developers and users on future changes to Kani, we decid
 
 You should create an RFC in one of two cases:
 
-1. The change you are proposing would be a "one way door": e.g. a change to the public API, a new feature that would be difficult to modify once released, deprecating a feature, etc.
+1. The change you are proposing would be a "one way door": e.g. a major change to the public API, a new feature that would be difficult to modify once released, etc.
 2. The change you are making has a significant design component, and would benefit from a design review.
 
-Bugs and smaller improvements to existing features do not require an RFC.
+Bugs and improvements to existing features do not require an RFC.
 If you are in doubt, feel free to create  a [feature request](https://github.com/model-checking/kani/issues/new?assignees=&labels=&template=feature_request.md) and discuss the next steps in the new issue.
 Your PR reviewer may also request an RFC if your change appears to fall into category 1 or 2.
 
@@ -36,6 +36,9 @@ This is the overall workflow for the RFC process:
    2. Start from a fork of the Kani repository.
    3. Copy the template file ([`rfc/src/template.md`](./template.md)) to `rfc/src/rfcs/<ID_NUMBER><my-feature>.md`.
    4. Fill in the details according to the template instructions.
+     - For the first RFC version, we recommend that you leave the "Software Design" section empty.
+     - Focus on the user impact and user experience.
+       Include a few usage examples if possible.
    5. Add a link to the new RFC inside [`rfc/src/SUMMARY.md`](https://github.com/model-checking/kani/blob/main/rfc/src/SUMMARY.md)
    6. Submit a pull request.
 2. Build consensus and integrate feedback.
@@ -44,22 +47,24 @@ This is the overall workflow for the RFC process:
    3. If the RFC is not approved, close the PR without merging.
 3. Feature implementation.
    1. Start implementing the new feature in your fork.
-   2. It is OK to implement it incrementally over multiple PRs. Just ensure that every pull request has a testable
-      end-to-end flow and that it is properly tested.
-   3. In the implementation stage, the feature should only be accessible if the user explicitly passes
-      `--enable-unstable` as an argument to Kani.
-   4. Document how to use the feature.
-   5. Keep the RFC up-to-date with the decisions you make during implementation.
+   2. Create a new revision of the RFC to add details about the "Software Design".
+   3. It is OK to implement the feature incrementally over multiple PRs.
+      Just ensure that every pull request has a testable end-to-end flow and that it is properly tested.
+   4. In the implementation stage, the feature should only be accessible if the user explicitly passes
+      `-Z <FEATURE_ID>` as an argument to Kani.
+   5. Document how to use the feature.
+   6. Keep the RFC up-to-date with the decisions you make during implementation.
 4. Test and Gather Feedback.
    1. Fix major issues related to the new feature.
    2. Gather user feedback and make necessary adjustments.
-   3. Add lots of tests.
+   3. Resolve RFC open questions.
+   4. Add regression tests to cover all expected behaviors and unit tests whenever possible.
 5. Stabilization.
    1. Propose to stabilize the feature when feature is well tested and UX has received positive feedback.
-   2. Create a new PR that removes the `--enable-unstable` guard and that marks the RFC status as "STABLE".
+   2. Create a new PR that removes the `-Z <FEATURE_ID>` guard and that marks the RFC status as "STABLE".
       1. Make sure the RFC reflects the final implementation and user experience.
    3. In some cases, we might decide not to incorporate a feature
       (E.g.: performance degradation, bad user experience, better alternative).
       In those cases, please update the RFC status to "CANCELLED as per <PR_LINK | ISSUE_LINK>" and remove the code
       that is no longer relevant.
-   4. Close the tracking issue.
+   4. Close the tracking issue.

rfc/src/template.md

@@ -1,4 +1,4 @@
-- **Feature Name:** *Fill me with pretty name and a unique ident. E.g: New Feature (`new_feature`)*
+- **Feature Name:** *Fill me with pretty name and a unique ident [^unstable_feature]. Example: New Feature (`new_feature`)*
 - **Feature Request Issue:** *Link to issue*
 - **RFC PR:** *Link to original PR*
 - **Status:** *One of the following: [Under Review | Unstable | Stable | Cancelled]*
@@ -10,47 +10,77 @@
 
 ## Summary
 
-Short description of the feature, i.e.: the elevator pitch. What is this feature about?
+Short (1-2 sentences) description of the feature. What is this feature about?
 
 ## User Impact
 
-Why are we doing this? How will this benefit the final user?
+Imagine this as your elevator pitch directed to users as well as Kani developers.
+- Why are we doing this?
+- Why should users care about this feature?
+- How will this benefit them?
+- What is the downside?
 
- - If this is an API change, how will that impact current users?
- - For deprecation or breaking changes, how will the transition look like?
- - If this RFC is related to change in the architecture without major user impact, think about the long term
-impact for user. I.e.: what future work will this enable.
+If this RFC is related to change in the architecture without major user impact,
+think about the long term impact for user.
+I.e.: what future work will this enable.
+   - If you are unsure you need an RFC, please create a feature request issue and discuss the need with other Kani developers.
 
 ## User Experience
 
-What is the scope of this RFC? Which use cases do you have in mind? Explain how users will interact with it. Also
-please include:
+This should be a description on how users will interact with the feature.
+Users should be able to read this section and understand how to use the feature.
+**Do not include implementation details in this section, neither discuss the rationale behind the chosen UX.**
 
-- How would you teach this feature to users? What changes will be required to the user documentation?
-- If the RFC is related to architectural changes and there are no visible changes to UX, please state so.
+Please include:
+  - High level user flow description.
+  - Any new major functions or attributes that will be added to Kani library.
+  - New command line options or subcommands (no need to mention the unstable flag).
+  - List failure scenarios and how are they presented (e.g., compilation errors, verification failures, and possible failed user iterations).
+  - Substantial changes to existing functionality or Kani output.
 
-## Detailed Design
+If the RFC is related to architectural changes and there are no visible changes to UX, please state so.
+No further explanation is needed.
 
-This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind:
+## Software Design
 
-- What are the main components that will be modified? (E.g.: changes to `kani-compiler`, `kani-driver`, metadata,
-  installation...)
-- How will they be modified? Any changes to how these components communicate?
-- Will this require any new dependency?
+This is the beginning of the technical portion of the RFC.
+From now on, your main audience is Kani developers, so it's OK to assume readers know Kani architecture.
+
+Please provide a high level description your design.
+
+- What are the main components that will be modified? (E.g.: changes to `kani-compiler`, `kani-driver`, metadata, proc-macros, installation...)
+- Will there be changes to the components interface?
+- Any changes to how these components communicate?
 - What corner cases do you anticipate?
 
+**We recommend you to leave this empty for the first version of your RFC**.
+
 ## Rationale and alternatives
 
-- What are the pros and cons of this design?
+This is the section where you discuss the decisions you made.
+
+- What are the pros and cons of the UX? What would be the alternatives?
 - What is the impact of not doing this?
-- What other designs have you considered? Why didn't you choose them?
+- Any pros / cons on how you designed this?
 
 ## Open questions
 
-- Is there any part of the design that you expect to resolve through the RFC process?
-- What kind of user feedback do you expect to gather before stabilization? How will this impact your design?
+List of open questions + an optional link to an issue that captures the work required to address the open question.
+Capture the details of each open question in their respective issue, not here.
+
+Example:
+- Is there any use case that isn't handled yet?
+- Is there any part of the UX that still needs some improvement?
+
+Make sure all open questions are addressed before stabilization.
+
+## Out of scope / Future Improvements
+
+*Optional Section*: List of extensions and possible improvements that you predict for this feature that is out of
+the scope of this RFC.
 
-## Future possibilities
+Feel free to add as many items as you want, but please refrain from adding too much detail.
+If you want to capture your thoughts or start a discussion, please create a feature request.
+You are welcome to add a link to the new issue here.
 
-What are natural extensions and possible improvements that you predict for this feature that is out of the
-scope of this RFC? Feel free to brainstorm here.
+[^unstable_feature]: This unique ident should be used to enable features proposed in the RFC using `-Z <ident>` until the feature has been stabilized.