>All imperative programs can be described by purely functional mappings between points in a program state space with each in scope variable naming a dimension.

... Using Predicate Calculus.

I said the same thing here: https://news.ycombinator.com/item?id=34206888

We Dijkstra fans have to stick together :-)