The unreasonable power of algebra

Professor Sir Tony Hoare ( Emeritus Professor of the University of Oxford and Consultant Principal Researcher at Microsoft Research (Cambridge) Ltd )

At the beginning of my academic career (1968), I wanted to express the axioms of sequential computer programming in the form of algebraic equations.  But I did not know how.  Instead I formalised the axioms as deduction rules for what became known as Hoare logic.

I now know how I should have done it as an algebra.  Furthermore, I can add a few neat axioms that extend the algebra to concurrent programming.  From the axioms one can prove the validity of the structural proof rules for Hoare logic, as extended to concurrency by separation logic. Furthermore, one can prove the deductive rules for an operational semantics of process algebra, expressed in the style of Milner.  In fact, there is an algebraic time-reversal duality between the two forms of semantic rule.  For me, this was a long-sought unification.

In conclusion, the axioms are measurably simpler than each set of rules separately, and more powerful than both of them joined together.

Needless to say, proofs of the above claims are simple and algebraic.

They were discovered with the aid of a series of interns at Microsoft Research in Cambridge.