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