Hoare Axioms are Mapcode Theorems

C.A.R. Hoare in 1969 suggested a set of axioms that may be used to build proofs of program correctness. Despite their general acceptability even after a period of 40 years the method suggested by Hoare is not generally taught and used.

Prof. Kesav Nori once suggested a possible reason why correctness proofs of programs are not more popular than they are. Natural languages that  have evolved over the course of years have too complicated a structure to study mathematically.  Programming languages, even though man-made, still are very complicated, and hard to study mathematically. There is a vast variety of programming styles and it is a daunting task to tackle each program and try to reduce it to a series of Hoare logic links.

The mapcode style of programming we suggest uses only a very simple program template: a single while loop. So it may not be so hard to reason about their correctness using Hoare rules. However, we can show that the Hoare rules can be stated and proved as theorems in  mapcode. An exposition is given here. This shows that any program that may be proved correct using Hoare rules, can also be proved correct using mapcode. At the same time this result suggests that we do not need to confine ourselves to Hoare rules: any argument that is correct in terms of set algebra may be used. We thus have a very simple way of proving programs correct.