Then you sit and pound on the core axioms and transformations to make sure they are correct. This is impossible, in the strictest sense, but it is often practical.

All programs are mathematical proofs of one sort or another, so in the end, it's the same problem that every programmer faces: How do I know this program isn't buggy? Well, you don't, and yet, here we are, with broadly functioning programs of great complexity. Ultimately, going through a rigidly mechanical proof is a quantitative change, in that it takes your confidence in the lack of bugs from less than 100% to another value much closer to 100% but still lesser, but as I like to say, a large enough quantitative change is a qualitative change. So while it is true that the proof may not be 100%, that doesn't mean it would be useless.

Also, it should be pointed out that in the real world there is a real error rate that real CPUs have; a percentage of computations will go wrong. Pushing your confidence of your algorithms below that point is largely useless. In the real world, the difference between 10 or 15 9s and actual, factual 100% isn't actually relevant, so the fact that the proofs can't get to 100% is a much lesser concern than you might think. It would only matter if we had 100% reliable computers in every other way. I think I can safely say that the dominant problem in computing today is not unreliable hardware, though, it's bugs in our algorithms, so this is the right approach. (Note I said dominant; massive server farms have to worry about unreliable hardware, but even then, you'll be handling that with algorithms and code and your dominant problems on that front will be bugs in the code.)