That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all

That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.