What's the equivalent of a bug by the Curry-Howard isomorphism?

Question

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.

Answer 1

Unfortunately I don't think Patrick87's is fully correct. It is important to understand what is meant by "bug" in the question. I assume that "bugs" include errors affecting the types and errors that don't.

It is fundamental to note that under the correspondence, theorems relate only to type characteristics of a program, not values characteristics. So program statements such as x := x + 1 and x := x + 2 are completely equivalent from the theorem view. It is important to realise that in the normal interpretation these are just abstract theorems, these are not theorems about the program (for example about its correctness).

So from this it's easy to see that a lot (maybe most) bugs won't affect the corresponding theorems at all. For example if we have a financial program and we want to calculate net profit from gross profit, it could be correct to write NetProfit := GrossProfit * 0.8. But we might enter a bug and calculate the tax instead NetProfit := GrossProfit * 0.2. It has no effect on types so it has no effect on the correspondance. Many, many real bugs are like this: off-by-one errors, overflow errors, misunderstanding a subroutine's behaviour, numeric and string typos...

For bugs that do affect the correspondence, it depends whether they result in a valid theorem or not. If it results in a valid theorem, it's more likely that your program will compile, run without crashing etc. However, it means you got one of the types wrong, an example is if you want to put 2 numbers together, like 1 and 3 -> 13. But you forget to convert them to strings, so instead you get 1 and 3 -> 4. On the other hand, if it does not result in a valid theorem, then it means you probably got something seriously wrong, and the program won't compile, or it will get stuck in an endless loop, or something like that.

To summarise, if you have a program with a corresponding theorem that is valid, that doesn't tell you much. The program can still have bugs. On the other hand, if you are trying to make a program that doesn't have a corresponding theorem, then then that is a good indication you are probably going wrong. So it depends on the kind of bug, most don't show up at all.

Answer 2

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.