But if that makes it math, then a C program is also math.
It is the case I think. It's an imperative algorithm description language like CCAL. It might be translated into pure mathematical terms
using a "temporal logic of actions" symbolism. It is not expressive enough to be used comfortably to specify or to
exchange ideas as you have shown it but it's all mathematics.
To put it into Pfenning's words every time you have a different kind of logic you have a class of program languages. There's an isomorphism.
--
FL