[Izkata]

The thing that's always bothered me about this argument is the translation between proof and code+underlying system. Bugs can still be introduced there. Certainly significantly fewer bugs in the final result, but I don't think I'd be confident in calling it proven 100% bug-free.

[piano]

In languages with termination analysis and dependent types, the source code _is_ the proof and it's verified by the compiler. Basically when such a program compiles, it's proved to be correct according to the specification.

Of course this still leaves space for bugs outside the program itself which still may influence it, such as bugs in the operating system or firmware or the like. Which may be prevented by having a formally verified OS too :)

But even in such a case, there might still be hardware errors (electrical noise, for example). Which is why for example spacecrafts or critical industry machinery double or triple their whole architectures. In such case the formally verified software runs on eg. three instances simulatenously and these instances cross-check each other's results all the time. When a hardware fault occurs (a bit randomly flipped in memory for example), they find out they're not matching and re-calculate.

That's as close as you can get to zero bugs.