Comment 1:

I don't think any spec or syntax change is needed.  As you say, you can already
guarantee the behaviour you want with more awkward syntax, so I don't think we need to
add another kind of syntax for it.  In general, though, the compiler should generate
better code for this.

Labels changed: added release-none, repo-main, suggested.

Comment 2:

Note that for the following loop:
for _, v := range s {
  ...
  foo()
  ...
  use(v)
}
you can't generally prove (w/o global analysis) that it does not modify elements of the
slice. Because foo can be:
func foo() {
  c <- true
}
And the other side of the chan can be:
for i := range s {
  <-c
  s[i] = 0
}

/cc @rasky for possibility of doing this in the prove pass.

Could you provide a short example? I can look into whether this would fit into the prove pass.

I don't know much about it, but maybe the copyelim pass would be a possibility?

Would this currenlty be possible earlier on in walkrange (

I don't think this fits prove.

I don't think this fits prove.

Agreed. The more I read about RVO and copy elision, the more I think it's not for prove.