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.

*ASIDE*: The three fundamental studies were the *Tri**v**ium grammar* (words), logic (reasoning), and rhetoric
(effective communication). These allowed study of the QuadTivium arithmetic (patterns in number), geometry (patterns in space), music (patterns in tone), and astronomy (patterns in time). All
together, these subjects comprise the seven liberal arts.

These issues are of course still with us today. And while it might be difficult to codify real-world arguments about (say) gun-control laws, programs can be fully formalized, and correctness can be specified. We'll look at three examples where formal proofs are applicable:

- playing a simple game, WaterWorld;
- checking a program for type errors;
- circuit verification.

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. Optimizing compilers prove that, within your program, some faster piece of code behaves the same as and can replace what you wrote. With software
systems controlling more and more life-critical applications, it's important to be able to **prove** that a program always does what it claims.

- 577 reads