So, do you mean that in the above loop example, it would require you to prove somehow that the loop always finishes, or if the programmer fails to do that, fail

So, do you mean that in the above loop example, it would require you to prove somehow that the loop always finishes, or if the programmer fails to do that, fail with "possibly infinite loop" error? In what language/system you would require that proof?