Checking a variable is ever assigned to is a costly, and sometimes almost impossible.
But we can do this cheaply for the finals described in this proposal.

Another benefit of #29422.

@go101, assuming you're claim that this is "costly, and sometimes almost impossible" is true, that doesn't bode well for your proposal which relies on this type of analysis being possible by the compiler (to enforce the proposed new language semantics).

I should also note that addressing this in the compiler need not a rigorous proof of correctness that a full blown proposal like #29422 would require. If the compiler is ever unsure whether the variable is mutated, it could always do the safe thing, which is to emit bounds checks.

I think there are really some cases where the author of the code can make sure a global value will never be modified but it is difficult for compilers to deduce the same conclusion.

For a simple example, if a global slices are passed as arguments to many functions, and these functions continue to pass the corresponding parameter to many other more functions. I would be costly for compilers to deduce whether of not the slice will be modified.

I mean it is not bad to let compilers to deduce some global slices are never modified (if the deduction work is not costly). However, it would be better also let code author to tag some values will never be modified.

The optimization passes, including the removal of bounds checks, are done on each function independently. Have you tried an example where all aspects of your issue are in the same func?