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 Trivium 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.
- 瀏覽次數：1450
