I think this is saying that arrays are immutable at runtime and the bounds of the array are checked on compile. By doing this, loops can be checked before exec

I think this is saying that arrays are immutable at runtime and the bounds of the array are checked on compile. By doing this, loops can be checked before execution to prevent infinite loops and so constrain that as a Turing Machine construct. I think the underlying good idea here is that Turing Completeness is maybe overrated. You could argue that most good programming languages are good because of what they don't let you do - constraints around how state is mutated is core to Object-oriented and functional programming. Adding some more constraints to ensure complete and reliable static analysis sounds like an excellent idea to me.