Dijkstra's approach would be to prove there is a strictly decreasing natural number associated to the loop.

This limits programs to the ones that can be formally shown to terminate. Which is good enough for most purposes.

My approach is to accept programs that run forever as long as I'm fairly sure each loop makes progress of some sort (instead of simply doing "while not solved: continue").

Edit: There's also a fun algorithm that, as far as I know, only provably terminates by being bounded by a sequence of strictly decreasing ordinals. Which breaks all kinds of models for proving it terminates.