[johnbender]

> In general you can't prove a program will or won't terminate.

As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it terminates. It’s definitely possible to prove this manually per program and most dependently typed languages will do the work for you as a matter of sound over approximation as long as one of the arguments is shrinking in an obvious way.