That's a category error. The formal spec isn't a proof, it's what is to be proven. Without a spec the notion of programming errors has no formal meaning. In that case, the complaints about the bug are always with respect to pleasantness. Given a formal specification, it's possible to write a program that will reliably satisfy that specification. And the tooling is better than ever. The Dafny language out of Microsoft Research is one interesting example. One can also do it by hand, possibly using an SMT solver to check one's work.