Simply put, the Curry-Howard correspondence states that a type is a theorem and that a program returning this type is a proof of the corresponding theorem.
The correspondence is based on the formalization of mathematical proofs, in languages such as predicate calculus, restrained to intuitionistic logic. But when mathematical proofs are written in those formal languages, their errors can be detected by computers. For example, Mizar is a relatively high-level mathematical language, plus a compiler that checks the proofs written in it.
So Curry-Howard associates programs to mathematical proofs without errors. Therefore, how does Curry-Howard translate the concept of a program bug in the mathematical world ? By what's above, it's not a logical error in a proof.
Programs with bugs correspond to correct proofs which are different from the proofs to which the programs would correspond without the bugs. In other words, programs with bugs correspond to correct proofs, but different proofs. By way of analogy, a path is a particular sequence of steps you take out your front door. You may intend to walk the path to the grocery store. Perhaps you take a wrong turn and end up at the barber shop. You have still walked a path, just not the one you wanted.
Logical errors in proofs are more akin to runtime or syntax errors in programming language. In such cases, it's not that you have computed, proved or walked the wrong thing; but that you have failed to compute, prove or walk anything at all. In our analogy, this might be like forgetting how to walk and trying to take a few steps using only your left elbow and chin. You will not be able to complete your path - any path, right or wrong - because you attempt to do something that doesn't count as stepping.
An interesting challenge you might consider - write a correct, valid algorithm which is not correct for any possible problem.