What good are proofs?

Examples of proofs

WaterWorld Consider a game called WaterWorld, with the following rules: You are an explorer in a sea full of pirates. Whenever you enter a location, you need to declare wehther or not there is a pirate there; If you enter pirate turf without gold, you'll be killed, and conversely if you enter an empty location laden with gold, you'll sink. a single mistake will do you in. When you successfully enter an empty location, you can determine how many (of the up to three) neighboring contain pirates, though not necessarily which ones. When you successfully enter a pirate location, you get no information, but are allowed to live. We wish to know whenever we have a guaranteed safe move. For instance, in this board, add picture of a sample board are there any safe moves? What is your reasoning, that they are safe? How about in this next example?

Type Checking When writing a program, we'd like to know be sure that functions are being called with (at least) the correct type of inputs (e.g. the function + should be called with numbers (not booleans), and a function which a programmer has declared to return an integer really should always return an integer). Of course we'd really like to know whether the program has any bugs at all; type errors are only one sort of possible programming error. And we'd like to be sure of this before running the program. Consider:


	    int SEEMS_LIKE_FOREVER = 24;  // Time enough to procrastinate.
	    
	    // goSeeMovie?:
	    // When invited to see a movie, do you accept?
	    // Depends on how many hours until homework is due,
	    // and on how much time is needed to do the homework.
	    //
	    bool goSeeMovie?( int hrsTilHwDue, int timeNeeded ) {
	    if (hrsTilHwDue >= SEEMS_LIKE_FOREVER)
	    true;
	    else
	    (hrsTilHwDue >=timeNeeded);
	    }
	    
	    // Example: 
	    //   goSeeMovie?(  8,  8 ) = false
	    //   goSeeMovie?( 48, 48 ) = true

One reason programmers are required to declare the intended type of each variable, is so that the computer (the compiler) can prove that certain errors won't occur. How can you prove, in the above, that goSeeMove? really always returns a boolean value as promised? (At least, presuming that it is called with integers, as indicated. Likewise, you might want to later prove that whenever it is called, the provided integers are indeed provided.) (That is, what work does the compiler's type-checker do?)


	    int SEEMS_LIKE_FOREVER = 0;
	    
	    bool goGetRootCanal?( int hrsTilHwDue, int timeNeeded ) {
	    if (hrsTilHwDue >= SEEMS_LIKE_FOREVER)
	    true;
	      else if (hrsTilHwDue > SEEMS_LIKE_FOREVER)
	      timeNeeded;
	    else
	    false;
	    }

Note that most compilers will not accept this second example as valid code, even though is is possible to prove it's safe (if you know some math axioms about how >= and > work). (It certainly deserves to be caught by the compiler as poor code, just not as code that will generate an error.) In general, compilers tend to focus on simple type-checking and very limited checking for other bugs; we'll see in the future there is some reason for this. add link to halting prob, and mention completeness some type systems, in previous aside

Circuit Verification Given a circuit's blueprints, will it work as advertised? In 19__, Intel had to recall get numbers, ian ... of its Pentium processors, due to a mistake in the circuit: it didn't always add numbers correctly, for all inputs. This cost ...s of dollars, lots of bad publicity, and it happened after intensive testing. Could it have been possible to have a program try to prove the chip's correctness or uncover any errors? Software and hardware companies are increasingly turning to the use of automated proofs (rather than semi-haphazard testing) to verify (parts of) large products correct. It is a difficult task, which is also an active area of research.

Having proofs of correctness is not just comforting; it allows us to save effort (less time testing, and also able to make better optimizations), and prevent recall of faulty products. But: who decides a proof is correct -- the employee with best SAT scores?!? Is there some trusted way to verify proofs, besides careful inspection by a skilled (yet still error-prone) professional?

How can we tell true proofs from false ones? What are the rules of a proof? (Clearly, this is relevant to writing programs -- at least, bug-free programs.) These are the questions which will occupy us.

"Yeah, well prove it!" Compare the following proofs: All people are mortal. Socrates is a person. Therefore, Socrates is mortal. All [substitution ciphers] are [vulnerable to brute-force attacks]. The [Julius Caeser cipher] is a [substitution cipher]. Therefore, the [Julius Caeser cipher] is [vulnerable to brute-force attacks]. Note that you don't need to know anything about cryptography to know that the conclusion follows from the two premises. (Are the premises indeed true? That's a different question.) Use a lewis carroll example? All griznoxes chorble happily. A floober is a type of griznox. Therefore, floobers chorble happily. You don't need to be a world-class floober expert to evaluate this argument, either. As you've noticed, the form of the argument is the same in all these. If you are assured that the first two premises are true, then w/o any true understanding, you (or a computer) can automatically come up with the conclusion. This classical form happens to be called a "syllogism" (though the name isn't important). Even less important is knowing that some people have given names to each of the three steps: The major premise, the minor premise, and the conclusion. The point is that a syllogism is one example of a rule of inference -- that is, a rule that a computer can use to deduce new facts from known ones. make "rule-of-inference" into define tag? Mistakes in syllogisms are hard to make: what are the only two ways to have an error in a syllogism? The argument isn't actually in syllogism form. All people don't know my file's password. Equivalent to "Nobody knows my file's password". Why did we phrase this sentence awkwardly? Because a syllogism requires the first premise to be of the form "All somethings have some property". Any hacker is a person. Therefore, my file is secure from hackers. Not the correct conclusion for a syllogism. To be a syllogism, the conclusion would have to be "any hacker doesn't know my file's password." The file may or may not be secure, but the above doesn't prove it. One of the two premises is wrong. All people don't know my file's password. Is this really true? Any hacker is a person. Is this really true? Therefore, any hacker doesn't know my file's password. This proof fails of course, if some hackers are non-people (e.g. programs), or if some people know the password. (In fact, presumably you know the password!) add link: Example from The Cuckoo's Egg Male singer croons "Everybody loves my baby; My baby don't love [anybody] but me." Conclusion: the speaker is his own baby, and is narcissistic. (Or, the singer is wrong in his assumptions.) Of course, just because the argument fails, the conclusion might be true for other reasons. (That is, an incorrect argument doesn't prove the conclusion's opposite!)

Other rules of inference Of course, there are more ways to deduce things, beyond a syllogism; Who decides what the valid rules of inference are? Is it always clear when people have used the rules correctly?


	    +-----+-----+
	    |  1  |  1  |
	    | (A) | (B) |
	    +-----+-----+
	    |  ?  |
	    | (F) |
	    +-----+


	    +-----+-----+
	    |  1  |  X  |
	    | (A) | (B) |
	    +-----+-----+
	    |  ?  |
	    | (F) |
	    +-----+

Consider the following argument: (A) is next to one pirate; and (A) has only one explored neighbor; Conclusion: If you are a square next to (A), then you contain a pirate This conclusion is not true: (B) is certainly next to (A), but it doesn't contain a pirate. Alternately, consider that same proof applied to this board: Here, we know that (F) is safe, contrary to the conclusion. (In real life, I make this mistake all the time, when playing WaterWorld by hand! --The Author.) The problem is that the author of the argument presumably meant to conclude "all explored neighbors of (A) contain a pirate". Really, the underlying problem for this mistaken reasoning is These problems both arise, of course, because we were sloppy about what each sentence meant exactly. We used informal English -- a fine language for humans, who can cope with remarkable amounts of ambiguity -- but not a good language for specifying arguments. Laws and contracts are really written in a separate language from English -- legalese -- full of technical terms with specific meanings. This is done because, while some ambiguity is tolerable in 99% of human interaction, sometimes the remaining 1% is problematic. However, legalese still contains intentionally ambiguous terms (What is a punishment cruel and unusual? What exactly is the Community Standard of indecency?) The legal system tries to simultaneously be formal about laws, yet also be flexible to allow for unforeseen situations and situation-specific latitude. (And the result of this tension is the position of Judge.) In this course, we are trying to be entirely specific, with no ambiguity. We need to be more careful about how we state our facts, and how we use these known facts to deduce other facts. Note that such faulty reasoning might not just mean losing a silly game; it could result in a genuine software bug (prompting a $XXX chip recall, or giving faulty information to a medical doctor). One reaction to the above arguments is "Well, big deal -- somebody made a mistake (mis-interpreting or mis-stating a claim); that's their problem. (And sheesh, they sure are dolts!)" But as a programmer, that's not true: Writing any large system, human programmers will err, no matter how smart or careful they are. Thus we are looking for systematic ways to prove code correct or incorrect. Other fields have checklists, protocols, and regulations to minimize human error; programming is no different, except that the industry is still working on exactly what the checklists/training should be. The first thing we need is a way to say things without ambiguity. That's what we mean by a logic. In this case, we need a logic for the game of WaterWorld.