I see some tweets about "post-functional" as if functional were a cute trick that is passe. The world is already post-functional: imperative is post-functional: the lambda calculus is older than it all. Functional is not a cute trick: it is a profound consequence of Curry-Howard.
Russell and Whitehead's Principia Mathematica (1910) introduce a formal system for provability where, in modern terms, a proof is an automatically verifiable trace of execution of a non-deterministic automaton (which you may see going either from axioms to theorems or vice versa)
-
-
How would you argue that this trace corresponds to an imperative program?
-
In Russell-Whitehead, every sequential step of the trace carries the entire current state of the program. It is very much a big step operational semantics for an imperative language. The main side effects are non determinism and non termination / non totality.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!