A somewhat related idea is called "benign effects." The idea is that you write code with an immutable interface that uses mutation in its implementation. So th

A somewhat related idea is called "benign effects." The idea is that you write code with an immutable interface that uses mutation in its implementation. So there are "effects" (non-functional state changes) that are encapsulated ("benign"). I learned this term in reference to Standard ML at CMU. This is different from what you're asking because it isn't a compiler optimization and it isn't actually checked by the language at all, but it works pretty well in practice. It's like unsafe in Rust: you write most of your code assuming a useful property that you then break in the small percentage of code that needs to break it.