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.
-
Show this thread
-
Replying to @keithtpinson
Imperative is not a cute trick: it is a consequence of Russell-Whitehead, which predates the lambda calculus.
3 replies 0 retweets 5 likes -
Replying to @Ngnghm @keithtpinson
Do you have references on this correspondence?
1 reply 0 retweets 0 likes -
Replying to @FilippoSestini @keithtpinson
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)
1 reply 0 retweets 0 likes -
Replying to @Ngnghm @keithtpinson
How would you argue that this trace corresponds to an imperative program?
1 reply 0 retweets 0 likes
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.
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!