There is something of a movement in programming to make programs more
like proof systems, and computations more like proofs.  Coming in the
other direction there is similar enthusiasm in logic for making proof
systems more constructive, and proof more like computations.  There is
however the distinct possibility that the two movements will rush
right past each other and find that they have merely switched places!


Vaughan Pratt,
Dynamic Algebras as a Well-Behaved Fragment of Relation Algebras,
LNCS 425