[Tainnor]

> 1. There is no such thing as 100% accurate. Not only is it not physically possible (there can always be hardware errors or bit flips) but it's not even theoretically possible (you'd require a checker that was 100% accurate to tell, which is equivalent to solving the halting problem).

You don't have to solve the halting problem to prove a mathematical theorem (which includes proving things about a computer program), either manually or via an automated theorem prover.

One consequence of the halting problem (or more precisely, Rice's theorem) is that there is no algorithm that can determine a non-trivial property of an arbitrary program. It doesn't imply that you can't prove things about a specific program.

I suppose you can always be philosophical about it and say "how do I know the axioms are true" (whatever that means), or "how do I know there's no mistake in this proof" - but then you'd have to extend that same level of scrutiny to the theorem that the halting problem can't be solved, I guess.