Logics provide us with a formal language useful for
- specifying properties unambiguously,
- proving that programs and systems do (or don't) have the claimed properties, and
- gaining greater insight into other languages such as database queries.4
Programming language type systems are a great example of these first two points. The connectives allow us to talk about pairs and structures (x and y), unions (x or y), and functions (if you give the program a x, it produces a y). The "generics" in Java, C++, and C are based upon universal quantification, while "wildcards" in Java are based upon existential quantification. One formalization of this strong link between logic and types is called the Curry-Howard isomorphism.
Compilers have very specific logics built into them. In order to optimize your code, analyses check what properties your code has e.g., are variables b and c needed at the same time, or can they be stored in the same hardware register?
More generally, it would be great to be able to verify that our hardware and software designs were correct. First, specifying what "correct" means requires providing the appropriate logical formulas. With hardware, automated verification is now part of the regular practice. However, it is so computationally expensive that it can only be done on pieces of a design, but not, say, a whole microprocessor. With software, we also frequently work with smaller pieces of code, proving individual functions or algorithms correct. However, there are two big inter-related problems. Many of the properties we'd like to prove about our software are "undecidable" −−− it is impossible to check the property accurately for every input. Also, specifying full correctness typically requires extensions to first-order logic, most of which are incomplete. As we've seen, that means that we cannot prove everything we want. While proving hardware and software correct has its limitations, logic provides us with tools that are still quite useful. For an introduction to one approach used in verifcation, see TeachLogic's Model-Checking module.
- 1176 reads
