The halting problem is not a big deal in practice. Plenty of compilers for many programming/proof languages out there (Agda, Idris, Coq, LEAN etc.) will reject code that the compiler can’t prove is terminating. And yet those programming languages are more than powerful enough for writing real world software. Including operating systems, compilers etc.

A good introduction to this subject is the book “Type Driven Development in Idris” or one of the Agda books.