[andreasvc]

Choosing such a subset is not solving the halting problem. The halting problem says it is impossible to find a mechanical procedure that says whether an arbitrary program will halt. If a mathematician, by some intuition, is able to come up with a subset of programs for which some property can be proven, then this is not solving the general problem. Since this subset is not equal to the general set of programs, nor has it been found by some mechanical, formal means, it is not a violation of the theory of the halting problem. It can be a matter of a carefully crafted programming language, along with certain annotations (e.g., dependent types). Really, before making insistent statements like this, you should do some research (e.g. there's the whole field of program verification).