You realize that the common `debugging caveat' applies: computer do indeed do what we tell them to do. That doesn't mean than anyone understands what the computer are going to do.
Debugging sucks.
Formally verified code is not unheard of.
Formally verified code is awesome. It moves the `debugging problem' up one level, "Does our formal spec capture our informal meaning?"
Ideally in practice, that problem is simpler than "Does our code what we want?
In theory in the abstract, of course, the problems are the same.
There is no practical difference. Computers do what we tell them to do, whether what I tell it to do has a conditional in code (the computer chooses), or instead always chooses one option because I left that condition out is a completely irrelevant distinction.