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.
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.
-
-
I honestly don't know anything about this. I thought Russell and Whitehead's project failed.
-
Russell and Whitehead's project is vastly successful, and inspired all modern logic and mathematics. Certainly, they failed to achieve all their desired goals, but they also opened new domains nobody (including them) imagined existed.
- 1 more reply
New conversation -
-
-
Game Semantics breaks things down further with games, strategies, and plays. If a proposition is a game and a proof is a strategy + its plays, that's kind of Curry-Howard. If a proposition is a game + strategy and a proof is its plays, that's kind of Russell-Whitehead.
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!