The ancient Greeks loved to hang around on the stoa, sip some wine, and debate. But at the end of the day, they wanted to sit back and decide who had won the argument. When Socrates claims that one statement follows from another, is it actually so? Shouldn't there be some set of rules to officially determine when an argument is correct? Thus began the formal study of logic. Many other areas of computer science routinely involve proofs, although we won't explore them here. Manufacturing robots first prove that they can twist and move to where they need to go before doing so, in order to avoid crashing into what they're building. When programming a collection of client and server computers, we usually want to prove that the manner in which they communicate guarantees that no clients are always ignored.