Not "for any program", but "for an arbitrary program".
We can trivially prove that a program that always goes to the next step, without branching, always terminates. With more effort we can prove termination of certain segments with conditional jumps, certain forms of recursion and loops, etc. This is not purely theoretic: e.g. EBPF programs in the Linux kernel are only admitted if the kernel can prove that they terminahe.
What we can't do is to prove it in an arbitrary case, without putting limits on the program's structure.
We can trivially prove that a program that always goes to the next step, without branching, always terminates. With more effort we can prove termination of certain segments with conditional jumps, certain forms of recursion and loops, etc. This is not purely theoretic: e.g. EBPF programs in the Linux kernel are only admitted if the kernel can prove that they terminahe.
What we can't do is to prove it in an arbitrary case, without putting limits on the program's structure.