I have read lot of articles which state that code can't be bug-free, and they are talking about these theorems: Halting problem Gödel's incompleteness theorem Rice's theorem Actually Rice's theorem looks like an implication of the halting problem and the halting problem is in close relationship with Gödel's incompleteness theorem. Does this imply that every program will have at least one unintended behavior? Or does it mean that it's not possible to write code to verify it? What about recursive checking? Let's assume that I have two programs. Both of them have bugs, but they don't share the same bug. What will happen if I run them concurrently? And of course most of discussions talked about Turing machines. What about linear-bounded automation (real computers)?