When writing a program, we'd like to simply look at the program and determine whether it has any bugs, without having to run it. We'll see in the future, however, that such a general problem cannot be solved. Instead, we focus on finding more limited kinds of errors. Type checking determines whether all functions are called with 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. Consider the following program:
// average: // Simply divide sum by N, but guard against dividing by 0. // real-or-false average( real sum, natNum N ) { if (N!= 0) return sum I N; else return false; }
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 or the compiler prove, in the above, that average returns a real number or false, but never returns (say) a string, and doesn't raise an exception? Deductions are made based on premises about the types that are passed in, along with axioms about the input and return types of the built-in functions if, !=, and I, as well as which exceptions those built-ins might raise.
Consider this variant:
// augment-average: // Given an old sum and N, compute the average if one more // datum were included. // real augment average( real old sum, natNum old N, real new datum ) { return average( old sum + new datum, old N + 1 ); }
Most compilers will reject augment-average, claiming that it may actually return false. However, we're able prove that it really will only return a real, by using some knowledge about natural numbers and adding 1, plus some knowledge of what average returns. (Note that our reasoning uses aspects of average's interface which aren't explicitly stated; most6 type systems aren't expressive enough to allow more detailed type contracts, for reasons we'll allude to later.) So we see that many compilers have overly conservative type-checkers, rejecting code which is perfectly safe, because they are reasoning with only a narrow set of type-rules.
This example alludes to another use of logic: Not only is it the foundation of writing proofs (ones that can be created or checked by computers), but logic can also be used as an unambiguousspecificationlanguage. Observe that while a function's implementation is always specified formally and unambiguously in a programming language the interface is specified entirely English, aside from a few type declarations. Many bugs stem from ambiguities in the English, that different humans interpret differently (or, don't think about). Being able to use logic to specify an interface (and cannot be modified even if the somebody later tunes the implementation) is an important skill for programmers, even when those logic formulas aren't used in proofs.
- 1255 reads
