[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.