Ref Locals/Returns Language Feature Incomplete

[gafter]

Developing a language feature like ref locals and ref returns has the following among its subtasks

• Initial idea for the feature
• Draft (possibly informal) language specification detailing the working of the feature (see Proposal: Ref Returns and Locals #118)
  • Argument, evidence, or proof that the proposal is sound (e.g. does not result in active refs to stack variables that have gone out of scope)
• Compiler implementation of the feature as specified
• Draft specification for the set of changes to be made to CLI verification
  • Argument, evidence, or proof that the proposed changes are sound
  • Updated peverify implementation (Peverify needs to be updated for new ref-locals/returns rules #12285)
• Test suite demonstrating correctness of the static and dynamic semantics of the feature implementation
• Test suite demonstrating that the implementation produces code that obeys the modified verification rules.

Note that this list is not intended to be complete; it contains mainly items relevant to the issue. There are many other subtasks such as IDE support, debugger support, etc, that were included in the work to complete this feature.

The current state of the feature is that the implementation does not agree with the draft specification (see #10645) because of (undocumented) intended changes to the feature, and work has not yet started on the revised verifier rules, implementation, or testing to demonstrate that the compiler obeys the proposed rules. The latter test gap is a significant risk for this feature.