Yes and no.
In a fundamental sense, you're not solving the halting problem: you're just side-stepping it. You will be able to know whether every program in your language halts, but it won't be Turing-complete and the halting problem is specifically about Turing-complete languages. You've solved a different problem.
But in a practical sense, the answer is yes. By writing programs in a total language like this, you can confidentally answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering.
The question then becomes: how do you make a language like this practical? It's an active area of research called total functional programming and totality checking.
One interesting idea is that you don't want all your programs to halt: certain infinite loops (like an operating system's event loop) are actually healthy and useful. So total languages also have a notion of productive computation—roughly, programs that don't terminate but guarantee the creation of new output in finite time given new input. (Think online stream processing.)
Another interesting development is the idea of treating potential non-termination as an effect. In a sense, total languages are inherently limited¹. Not only do they express fewer programs than Turing-complete languages, but they also have unavoidable performance penalties². So it can still be useful to have parts of your program not be provably terminating. The solution, then, is to have some mechanism to restrict and explicitly mark these parts of the code, just like Haskell restricts and explicitly marks which parts of the code can do IO. You could do this by making totality checking optional for functions or by encoding Turing-complete programs in a type (ie a partiality monad) and having the function that runs those parts be a Turing-complete escape hatch in your language.
If you're interested in how this plays out in practice, take a look at Idris. It's a language similar to Haskell but total and dependently typed, designed with an eye towards writing programs and software engineering rather than formal logic and proof verification. It's still very much a research project, but one you can use to write actual programs. This answer on the CS StackExchange, written by Idris's creator, is a good overview of how it deals with totality checking and Turing-completeness.
Personally, I think these ideas are deeply exciting but still in the realm of research. Total functional programming and dependent types are becoming frieldlier and more usable all the time, but are still far out from practical deployment. (Even effect management à la Haskell is still a somewhat fringe idea in everyday software engineering!) But I'm confident that there is value here and that these technologies will become practical and used (but maybe not widely) in the next decade or so.
footnotes
¹ A specific limitation that can actually be relevant is that given some total language L, you can't write a full interpreter for L in L. See this discussion on the CS theory StackExchange for more details.
² I remember one of my professors mentioning that for any total language you can always construct a problem which can be solved but with asymptotics arbitrarily worse than a solution in a Turing-complete language. Unfortunately, I don't remember the name of the theorem, and might be getting some of the details wrong.
It's also not clear whether these catastrophically slower cases are ever interesting, or if they only come up in extremely contrived circumstances.
In a fundamental sense, you're not solving the halting problem: you're just side-stepping it. You will be able to know whether every program in your language halts, but it won't be Turing-complete and the halting problem is specifically about Turing-complete languages. You've solved a different problem.
But in a practical sense, the answer is yes. By writing programs in a total language like this, you can confidentally answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering.
The question then becomes: how do you make a language like this practical? It's an active area of research called total functional programming and totality checking.
One interesting idea is that you don't want all your programs to halt: certain infinite loops (like an operating system's event loop) are actually healthy and useful. So total languages also have a notion of productive computation—roughly, programs that don't terminate but guarantee the creation of new output in finite time given new input. (Think online stream processing.)
Another interesting development is the idea of treating potential non-termination as an effect. In a sense, total languages are inherently limited¹. Not only do they express fewer programs than Turing-complete languages, but they also have unavoidable performance penalties². So it can still be useful to have parts of your program not be provably terminating. The solution, then, is to have some mechanism to restrict and explicitly mark these parts of the code, just like Haskell restricts and explicitly marks which parts of the code can do IO. You could do this by making totality checking optional for functions or by encoding Turing-complete programs in a type (ie a partiality monad) and having the function that runs those parts be a Turing-complete escape hatch in your language.
If you're interested in how this plays out in practice, take a look at Idris. It's a language similar to Haskell but total and dependently typed, designed with an eye towards writing programs and software engineering rather than formal logic and proof verification. It's still very much a research project, but one you can use to write actual programs. This answer on the CS StackExchange, written by Idris's creator, is a good overview of how it deals with totality checking and Turing-completeness.
Personally, I think these ideas are deeply exciting but still in the realm of research. Total functional programming and dependent types are becoming frieldlier and more usable all the time, but are still far out from practical deployment. (Even effect management à la Haskell is still a somewhat fringe idea in everyday software engineering!) But I'm confident that there is value here and that these technologies will become practical and used (but maybe not widely) in the next decade or so.
footnotes
¹ A specific limitation that can actually be relevant is that given some total language L, you can't write a full interpreter for L in L. See this discussion on the CS theory StackExchange for more details.
² I remember one of my professors mentioning that for any total language you can always construct a problem which can be solved but with asymptotics arbitrarily worse than a solution in a Turing-complete language. Unfortunately, I don't remember the name of the theorem, and might be getting some of the details wrong.
It's also not clear whether these catastrophically slower cases are ever interesting, or if they only come up in extremely contrived circumstances.
About the Author
Tikhon Jelvis
consistency is all I askOperations Research in Haskell at Target
Studied Electrical Engineering and Computer Science at University of California, Berkeley
Lives in Berkeley, CA
8m answer views189.1k this month
Top Writer2017, 2016, and 2015
Published WriterSlate and Forbes