You want answers? / I want the proof! / You can't handle the proof!!

You're goddamn right Jessep ordered the code red. Kaffee got him to admit that. But if it wasn't for that, Kaffee would have to formally prove that Jessep did so, and he simply couldn't do that. It was a big risk on Kaffee's part.

In research, we often play a different game. Formal logic gives researchers a context onto which their results can be painted. With formal logic, we can show the ultimate limits of a process. We can show that certain configurations are actually OPTIMAL -- you can do no better. In the case of software, we can PROVE that software is bug free. As the problems we engineers and scientists face become more and more complicated, we draw upon mathematics even more. Unfortunately though, mathematicians through history have not been as rigorous in their statements as logicians. It has been adequate to say, "At this point, it should be clear to the reader that B follows from A," because the reader has always been an experienced mathematician that either can connect the dots from A to B or is well-read and knows of the chain of literature that can back this claim up.

However, as mathematics becomes more general and is needed to solve more of the world's problems, the disciplines it cuts into simply do not have that sort of experience. These disciplines call on mathematics because they need the CERTAINTY that can come with mathematical RIGOR. When a mathematician doesn't fill in ALL the blanks, some or all of the certainty is lost.

And so there's a new movement in proof methods. We're moving into the era of computer-aided proof and long-winded meticulous proofs that are accessible to ALL.

And that's what a recent article at Economist.com discusses. It's a short and good read.

Proof and beauty

The very last paragraph: (emphasis added)

Why should the non-mathematician care about things of this nature? The foremost reason is that mathematics is beautiful, even if it is, sadly, more inaccessible than other forms of art. The second is that it is useful, and that its utility depends in part on its certainty, and that that certainty cannot come without a notion of proof. Dr Gonthier, for instance, and his sponsors at Microsoft, hope that the techniques he and his colleagues have developed to formally prove mathematical theorems can be used to “prove” that a computer program is free of bugs—and that would certainly be a useful proposition in today's software society if it does, indeed, turn out to be true.