Even if we had an answer to the halting problem, from a practical point of view, it's solving the wrong problem anyway. There's no point in distinguishing a function that would run forever from one that would exit after a century. They are both too slow.

Knowing that functions terminate is important for proof languages like Lean, where you often want to prove things without running the code at all. You're proving that one could, theoretically, calculate an answer, without actually calculating it.