Semantic restrictions of immutable value (`let`) bindings

[josh11b]

1. Are we comfortable requiring no mutation of objects with a non-copy-value representation and an active let binding?
2. Do we expect our safety story to enforce this at compile time with our strictly safe dialect?
3. Are we comfortable making this erroneous behavior when we are unable to or choose not to enforce this requirement at compile time?
4. Are we comfortable deferring the decision of whether strict enforcement of this property is enabled in our current C++-friendly mode until our safety design is complete?

These questions were prompted by discussions on proposal #5434 .

[chandlerc]

Notably, this was a major topic of discussion in the open discussion with detailed notes here: https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.uot97ukynlsi

Not going to try to capture all of the concerns raised across these four points that were I think reasonably well covered over the course of the discussion. Mostly suggested filing the issue to capture any additional written thoughts and make sure we reach (and document) a decision.

[chandlerc]

My thoughts, somewhat disorganized, sorry.

• a) I think we should initially make mutation of objects with a non-copy-value representation in an active let binding erroneous behavior.
• b) I don't think we should ever make it anything more than erroneous behavior, because we don't need to. See my note on erroneous behavior below. If we can prove the mutation doesn't occur, then we can use that under "as-if", and we don't need anything else.
• c) I think we will always have potential for unchecked code that could in theory mutate due to unsafe code and C++ interop. This goes to my point about erroneous behavior.
• d) I think we should try to enforce the lack of mutation in the strict safe dialect.
  • We should only relax our stance here and consider making such mutation allowed if we discover difficulty with this that we cannot overcome.
  • But we should revisit the underlying idea of mutation being erroneous if enforceing it in the strict mode proves fundamentally untenable due to ergonomic costs.
• e) I am very comfortable deferring the decision of whether strict enforcement is enabled in our current C++-friendly mode.

---

On erroneous behavior: I don't think we should optimize on erroneous behavior, ever, unless the compiler literally proves that it does not occur, ever. In which case, we don't need any license to start optimizing on this, as it falls under "as-if". Which means I don't tihnk we should optimize on erroneous behavior, ever. We should only optimize on "as-if". The fact that UB provides "as-if" without a proof is precisely the risk of using UB for any semantics, and why we don't use it here and elsewhere we use erroneous behavior. I should probably write this up as a principle.

[chandlerc]

Leads are decided with this last comment and rationale.