>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 no

>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.