Lecture: Algebra, Logic, Geometry at the Foundation of Computer Science
C. Antony R. Hoare
Abstract:
I show by examples how the Theory of Programming can be taught to first year CS undergraduates. The only prerequisite is their High School acquaintance with algebra, geometry and propositional calculus. The students’ motive is to learn how to construct and debugs their programs.
I start with the familiar laws for disjunction in Boolean Algebra, illustrated by disjunction. A deductive rule for proof by cases is derived from the algebra. The algebra is extended by the operators of spatial and temporal logic: William of Occam’s ‘while’ (|) and ‘then’ (;). They satisfy the same familiar algebraic laws, including distribution through disjunction. A weak interchange law describes how they distribute through one another by ‘shuffling’. Proof rules are then derived for a modal logic of time and space.
If this logic is applied to propositions about the behaviour of programs, the ‘while’ and ‘then’ operations can be reinterpreted as sequential and concurrent compositions of programs. The proof rules of the modal logic are then definitionally equivalent to two historic logics due to Hoare and Milner. They are now used widely for mechanical reasoning about correctness of programs and about implementations of programming languages.
