To answer your two questions, it is possible to mathematically prove, using certain tools that are admittedly rather academic (my argument is that we should consider using them more), that certain behaviors are impossible in a program. For example, a buffer overflow, or some form of data leak. This has been done, though admittedly not to programs anywhere near as complex as, say, the Windows kernel.
And, if there's a bug in your math, you will, of course, have some bug. Garbage in, garbage out. But! You can write your mathematical proof in such a way that the computer checks it for you (for example, static typing is a weak form of this). So all you need to have faith in is that program. Now we've exchanged faith in all programs to faith in one program. Which is an advance. But then we can formulate a proof that that program is correct in its own proof language. We hand-check this proof once, and then from then on the program can check later iterations of itself.
That's the dream, anyways. Some of the machinery to do this is available today, but some not.