Home

Applications of Blockchain to Programming Language Theory

Let's talk about Blockchain. Goal is to use this forum topic to highlight its usefulness to programming language theory and practice. If you're familiar with existing research efforts, please share them here. In addition, feel free to generate ideas for how Blockchain could improve languages and developer productivity.

As one tasty example: Blockchain helps to formalize thinking about mutual knowledge and common knowledge, and potentially think about sharing intergalactic computing power through vast distributed computing fabrics. If we can design contracts in such a way that maximizes the usage of mutual knowledge while minimizing common knowledge to situations where you have to "prove your collateral", third-party transactions could eliminate a lot of back office burden. But, there might be benefits in other areas of computer science from such research, as well.

Some language researchers, like Mark S. Miller, have always dreamed of Agoric and the Decades-Long Quest for Secure Smart Contracts.

Some may also be aware that verification of smart contracts is an important research area, because of the notorious theft of purse via logic bug in an Ethereum smart contract.

By Z-Bo at 2020-04-13 14:38 | Fun | Implementation | Semantics | other blogs | 103745 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Cargo cult computer science

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

By israelrt at Mon, 2020-04-13 21:17 | login or register to post comments

Block chains and PL

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.

By dmbarbour at Mon, 2020-04-13 22:53 | login or register to post comments

The intersection of Game Theory and Game Semantics

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.

By François-René Rideau at Wed, 2020-04-15 23:50 | login or register to post comments

Thanks, fare

I was hoping you would chime in, as you're one of the leaders and visionaries in this area. Much appreciated.

By Z-Bo at Thu, 2020-04-23 14:47 | login or register to post comments