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.
-
-
Then why do imperative languages tend to be an amalgamation of cute tricks?
-
Bias in the observer. Bias in the observed. Correlation that isn't causation. Just because most languages suck, and most language happen to be "imperative", doesn't mean that "imperative" necessarily sucks.
- 4 more replies
New conversation -
-
-
This Tweet is unavailable.
-
I'm not saying you can't do things with Curry-Howard. I'm just saying Russell-Whitehead is not getting enough credit these days, and that the interplay between the two correspondences is an under-exploited fertile land.
- 3 more replies
-
-
-
Do you have references on this correspondence?
-
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)
- 2 more replies
New conversation -
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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!