ABSTRACT
Most of mathematics deals with statements that are known with certainty, or as least as much certainty as can be attained by fallible human beings. The statement “2+2=4” is the archetype of a statement that is known to be true. In a similar way, the objective in many types of computer software is to be entirely reliable, or at least as reliable as amachine that is built of silicon and is running a commercial operating system can be. Indeed, we don’t want compilers, or payroll databases, or control systems for nuclear reactors to give more or less correct answers most of the time-we want them to always work correctly. To a substantial degree, this is often an attainable goal.
