For instance, I can mathematically prove that 4195835 / 3145727 > 1.3338. However, I know of certain Pentium processors that would disagree with me. If I try to prove that the following bit of C code prints out "Hello World":
if (4195835.0 / 3145727.0 > 1.3338)I might be a bit surprised when it deletes my hard drive instead ;)
system("rm -rf /");
1 bunny + 1 bunny = 2 bunnies, right? Well it depends on their sexes. It's possible that in a given time period, 1 bunny + 1 bunny might equal 5 bunnies. As I joked in a previous blog post, "All models are wrong. Some models are useful."
I really think this same thing applies to proving programs. Donald Knuth famously said, "Beware of bugs in the above code; I have only proved it correct, not tried it."