Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. A loop where you don't have these things is almost certainly a bug.

The vast majority of loops iterate over some finite collection of elements and are thus guaranteed to terminate. Tricky cases are stuff like "I will repeat this operation until the output stops changing".

>Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination.

If you're making Space Shuttle software from scratch yes. In practice for 99% of current mainstream development you depend on piles upon piles of dependencies, which might or might not check those loop invariants correctly, or might have a (trivial to add) endless blocking timeout, a deadlock, and many other wonderful things.

Usually they're not even set in stone, you'll update to the next version, and if they introduced such an issue, there's lots of fun to be had.

Nobody doubted you can have formal proofs for algorithms, or checked software in certain conditions and for certain controlled environments (e.g. using MISRA C and such) (in fact, I support this in a comment elsewhere in this thread).

The objection is to the idea that this is applicable (or trivially applicable, and we just aren't doing it out of laziness or something) to regular software development.