Any imperative algorithm admits functional mathematical interpretations. While humorous, the observation that programming in C is purely functional[1] isn't wro

Any imperative algorithm admits functional mathematical interpretations. While humorous, the observation that programming in C is purely functional[1] isn't wrong. Also consider, for example, that the formalism for the Turing Machine, the archetypical imperative automata, is purely functional. More seriously, the semantics of an imperative algorithm are perhaps always best understood as mathematical functions. Predicate transformer semantics reduce verifying an imperative program to proving a first-order formula. Leslie Lamport, who most people doing so-called "formal verification"[2] know for TLA+, is also a shining light in this area of research. They are observably complementary cognitive tools for the task of writing correct programs, even if one is attracting more grants. The trick is learning to write programs that reduce to formula that can practicably be solved, automatically or not. Granted, for many languages that first-order formula might be difficult to solve for many programs, but that doesn't change the fact that there exists a functional description of the procedure's semantics, even if the process the hardware actually executes isn't so analyzed[3]. But then that's true for Haskell too. It's just Haskell and its cousins do a comprehensive job of beating you over the head that you're reasoning about program semantics and not processes. [1] http://conal.net/blog/posts/the-c-language-is-purely-functional http://conal.net/blog/posts/the-c-language-is-purely-functio... [2] Correctly it should be called automatic verification. Formal reasoning predates the automatic computer and automatic verification is a subset of mathematically rigorous formal program verification. [3] Not to say it necessarily can't be.