Moreover, the halting problem doesn’t show that the set of programs you can’t decide halting for is in any way interesting.
It’s a constructive proof, yes, but it constructs a peculiarly twisted program that embeds its own proof-checker. That might be relevant for AGI, but for almost every program in existence we have no idea which group it’s in, and would likely guess it’s provable.
Moreover, the halting problem doesn’t show that the set of programs you can’t decide halting for is in any way interesting.
It’s a constructive proof, yes, but it constructs a peculiarly twisted program that embeds its own proof-checker. That might be relevant for AGI, but for almost every program in existence we have no idea which group it’s in, and would likely guess it’s provable.