If you read the proof of that theorem, you'll see it's irrelevant: the decidable set, while "asymptotically dense" does not contain most programs humans write. But in any event, halting itself is not very interesting. The point is that knowing one property (like halting) cannot help you with others.

As to whether the class of programs humans write are theoretically feasibly verifiable, nobody knows for sure, but the problem is certainly not easy, judging by all attempts so far.