I can definitely see them being philosophical, but I think that the actual question is what is needed for “real” software, not what can be proven correct. What fraction of software can you write with for-each style repetition constructs and no infinite collections? (Implicitly you can’t have recursion in that question either.) If you only have finite iterations, the halting problem is solved as everything halts. I haven’t looked into it, but I’m guessing that subset of programs might also be completely provable. The question is whether it is sufficiently powerful to do what we need. That question almost certainly lacks a nice clean answer.