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.
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.
Read my blog!