[capicue]

From a theoretical perspective, preventing infinite loops is in a very deep sense the most basic possible thing you can do with static types! The simply-typed lambda calculus, on which all other type systems are based, proves that programs terminate in a finite amount of time.

Is this not claiming that static typing (and/or lambda calculus) solves the halting problem?

[tikhonj]

No. Rather, some typed variants of the lambda calculus are not Turing-complete. They prevent infinite loops without running into the halting problem by being strictly less powerful than normal programming langauges.

It's worth noting that this is not an either/or problem. Some modern dependently typed languages take a more nuanced approach: they have a less-powerful core with enforced termination¹ and a way to write potentially non-terminating code that's isolated from everything else by the type system. It's the same approach that Haskell uses successfully for IO—it allows IO, but only in a controlled and explicitly delimited part of the program.

In a very real sense, we can treat potential non-termination as yet another effect and manage it accordingly.

¹ Actually, they're even more nuanced than this: programs either have to provably terminate or be provably "productive", which means they produce some new output from new input in finite time. This allows languages to support beneficial infinite loops like the event loop in an operating system while preventing purely harmful busy loops that never get anywhere.

[sharkbot]

Far from it; rather, that the simply typed lambda calculus is not Turing complete. One cannot represent a Turing machine in the simply typed lambda calculus, exactly because non terminating programs cannot be expressed.

One can add a fix point to the calculus (such as the titular Y combinator), but that introduces inconsistency to the type system.

[hawkice]

What is actually happening here is not quite what you think. There is a subset of programs for which you can prove it halts, notably lower-bounded by e.g. Idris' totality checker (which is a part of its type system).