Lambda the Ultimate

I understand that it falls under the purview of the Proceedings of Cargo Cult Computer Science and abstracts are published on Twitter....

From a PL perspective, a block-chain is essentially a very slow, expensive, shared, addend-only log with relatively weak tolerance to network partitioning. I'd be much more interested in application of CRDTs to PL designs for survivable networked systems.

There is a reasonable question of what sort of languages should be computed in context of the block-chain. That is, the converse of your proposed topic: applications of programming language studies to design of computation models for block-chains. Guarantees for progress, static allocation, static latency constraints, some type models that correspond to things people want to actually talk about (e.g. linear types for trade, linear numeric types to represent fungible commodities, bounties, signature types, units of measure).

Block-chains are a relatively inefficient substrate for expensive computations. So, the sort of problems in NP might better be turned into 'async effects' of sort, where we propose the problem with a bounty, verify the solution (in polynomial time), then continue with the contract. Similar 'effects' might include obtaining sign-offs from users, or requesting signed and dated data from a third-party server to continue a computation. But we might need to first share a hash of the solution to protect attribution, prevent the solution from being stolen. And we might need to 'claim' the effort to find a solution or make a request, to avoid redundant async efforts when there is only one bounty. I think perhaps the handling of 'effects' from a block-chain computation is the most interesting constraint from a PL design perspective.

I have been in the space of programming languages for blockchain for two years now. See my latest startup Mutual Knowledge Systems, its programming language Glow. For an introduction, the videos on our website. For details, the whitepaper. For more information, the articles I posted on medium.

What makes the space interesting is that it is about interactions between people who don't trust each other, so that the usual assumptions about correctness (that all the parts of a program conspire together towards the desired result) don't hold. Instead, you must go back to Game Semantics and Game Theory, and that makes the entire field richer and more interesting. Also harder, because your bug tolerance is 0.