Code as Theory

For several years now, together with many people, I have worked on new mathematical foundations for game theory and decision theory.¹ These foundations are based on tools and methods from semantics, a branch of theoretical computer science.

Now, I am an economist and I hang out with economists quite a bit. I often get the question, “What are you actually doing?”, followed by the comment, “this looks very strange to me”, and eventually followed by the question (anticipating a negative answer), “Is this economics at all?”. I understand the reaction. Our technical papers are hard to swallow as they use language foreign to most economists. The fixed costs required to make sense of their content is high.

In this post, I give a non-technical perspective on why I think what we do is relevant. The short answer: It is at the core of what digitalization means for economic theory. More and more economic activity happens on software systems. These systems are designed. We are bridging the gap between specification based on economic models and implementation in code.

Economic design

For a long time, economists have been rather passive observers of markets. Only since recently, some of them have begun actively designing allocation systems (for an overview and many resources see Market Design Blog).²

This trend is heavily influenced by the digital transformation. More and more marketplaces are implemented through code. Code is written by someone. And whoever that is makes design decisions which restrict the allowable behavior within the system. When the software implementation contains the possible economic behavior, then we can study economic concepts by analyzing software and the interaction of users relying on that software. Understanding the connection between code and behavior also helps us to design such systems.

The research program I purse together with my coauthors lifts economic concepts to the study of programs. How programs behave and what processes they generate is one of the core problems in the field of semantics. We use methods developed therein to describe programs and give them an economic interpretation – typically based on decision theory and game theory. There are various exciting aspects about this. But here, I will focus on the question how it helps to design economic software systems. To that end we need a little detour.

Programs and processes

A (very) simplified picture of a software design process is the following:

Specification ↝ Program ↝ Process

In the context of economic design, the specification will often follow from an economic model, say an auction.

Economic Model ↝ Program ↝ Process

The squiggle arrow indicates that the transformation from left to right is everything but straightforward. First, consider the process that a program exhibits. Most code is buggy at some point. This ranges from the obvious errors where our code does not compile to the less obvious ones when our software does not do what it is supposed to be doing.

The second problem is the translation from specification into program. This connection can be loose. And the loser the connection the more likely are we to make mistakes and waste resources. For many applications it is not clear what the “correct” specification should be. But for an economic allocation problem we may have something very specific: a formal model. This should ease the translation, shouldn’t it? Yes, however, there are still many issues to deal with. To begin with, the implementation of an economic model in standard programming languages is not completely determined by the theory.

For one, software often requires much more detail than is delivered in economic models. Take a game where players act simultaneously. What does simultaneous mean? More generally, how do we deal with time? Second, mathematical properties of economic models do not always directly translate into code. A simple but still profound example is the representation of real numbers which are ubiquitous in economic theory. Third, we will choose a specific economic model as the foundation of our specification because we can derive certain properties for it. For instance, we may want to implement a second price auction because we know, under certain assumptions, an equilibrium exists where each agent bids truthfully his evaluation. But how can we make sure that the system we then implement does faithfully represent the theoretical object with all its properties we had in mind? In the worst case, it will exhibit different incentives which may be a way to manipulate the auction.

What can we do about it? One approach: many, many iterations. The hope is, after enough time, the code will converge to its correct version and the specification we have in mind. But what do we do when we do not have enough time? Or when many iterations are not feasible? Or when the stakes involved are very high? For instance, in a blockchain, by design, we may not be able to change the initial code. Obviously, we can iterate across different blockchain systems and accept the death of some as the nature of the game we play. Or we start looking for an alternative.

Programming and mathematical language

How can we make software design more robust? One route, often associated with semantics, is to strive for a formal description of how a program behaves. Why mathematics? Mathematics gives us precision and allows us to prove things. In the ideal world, the program resembles mathematical statements which we know to be true. Where this is possible, code becomes more robust.³

In the last decades, a lot of progress has been made in developing these mathematical foundations. As a result of this effort, we have seen the development of new functional programming languages like Haskell and Agda which are closer to a mathematical ideal. In parallel to that, people have developed tools for formal verification: This means that properties of the specification as well as the correctness of the code can be proven with the help of a machine (See here for a nice overview). What is relevant for us, and possibly news to economic theorists, we can think about programming in mathematical useful ways. Once we consider the right mathematical language, code and the resulting process implemented by it are tightly linked. This can be expressed as:

Program ↔ Process

The interface to economics?

What does this have to do with economics? Our interest here is in specifying economic systems and ultimately economic processes. While achieving a tighter connection between program and process is of help to reduce errors, still this only gets us so far. The specification is still only loosely connected to the program:

Economic model ↝ Program ↔ Process

But now, given that we have a formal underpinning of the program and our economic models are expressed in math as well, we can start looking for a translation between the two. If we achieve a formal translation between model and program, then we can be confident that our system is a faithful representation and will exhibit the properties we want it to have:

Economic Model ↔ Program ↔ Process

In this case, the specification language is such that a direct translation to code is possible. If we keep up the tight relation between code and process, we get what we want. This means, once we verify that our model fulfills a relevant property, we know our implementation does so as well.

Achieving an equivalence between model, code, and process, is appealing in theory. But can it be achieved at all? A first look at the mathematical languages used in economic theory and in the foundation of programming in computer science unveils a huge mismatch. It is all but clear how to formally go between these two domains. Conceptually, the biggest difference is the process orientation in computer science, which arises naturally from the need to model computations which evolve over time.

Yet, there is another way. While it may not be possible to translate back and forth starting with the formalisms as is, we can try to reformulate economic theory in the more abstract mathematical language of computer science.

That is what we have been working on in the past years and what we have at least partially achieved. See here for more details.

So what?

This is all nice. But why should we care? One answer is not specific to economics but concerns a general problem in software design. When our possibilities to iterate over different shipped software versions are limited; systems get so complex that testing of components is of limited help; or bugs have massive consequences, then more formal approaches to software design may help. This is not a panaceas but for some applications it makes sense – including economic allocation systems. Expressing economic concepts in a language that can be directly implemented helps to increase the reliability of software and reduces development time.

One example where a more formal approach makes sense is the blockchain. First, some blockchain applications clearly serve economic goals. Second, as it is harder to change the codebase once the blockchain is implemented, it is important to get the implementation correct right from the start. Lastly, if we make mistakes, errors can be dramatic and hard to be undone. Overall the blockchain requires a high quality implementation. Of course, high quality software is not only relevant for blockchain applications. Virtual economic allocation systems will become central to modern economies. The more we rely on such systems the more we need to care about the quality of their implementation as part of our everyday infrastructure.

But what’s the implication for economic theorists? All what I described above is far away from what they do and what they care about. Should they deal with the details of implementations? This would seem odd. After all, market design, the field of economics which deals with the design of markets, has flourished. Within the whole field of economics, it is probably the only area where PhDs get hired for what they know about economic theory by private companies (see here). And they are rarely hired for their ability to implement stuff. So forcing them to deal with implementations appears as a regression. In addition, computer scientists, in particular those with a background in algorithmics, have adopted game theory themselves – to a point where many exciting developments are coming from their end (for an overview, see here). And of course, they know how to implement stuff.

So, for the record, no, I do not want economists to deal with the details of implementation. In particular not “applied” theorists. They should focus on economic questions. That is the whole point of our approach. We aim for a formal language to express economic concepts so that questions of implementations are already dealt with (as far as this is possible) – a domain specific language if you like. For sure, the language looks different from what theorists know, it may have some additional constraints but it will also be more expressive in other dimensions – we already know that. In the end, this is still economic modelling. From an applied perspective, it will make economic modelling much more practical. It will empower economists to find solutions which have bearing on applications as what they do will be (in principle) implementable. At the same time, the same feature will serve as a disciplining filter. As far as a model is not useful, it cannot be blamed on the wrong interpretation or implementation. It’s the model, stupid!⁴

We do no have a magic bullet and our framework is far from settled. At this stage, following our approach will limit the questions economists can pose. There are many important issues outside its scope and there is theory which is not operational but still valuable. But in a world that gets eaten by software, theory which is not implementable and claims to be practical will become more and more obsolete.⁵ Go back fifteen years and ask what a stable monetary policy is. You get all sorts of models and answers. Today, we see startups attracting funding because they promise to deliver a stable cryptocurrency. The old answers may help but they are not enough, as whatever makes such a currency stable – in so far as this is possible at all, must be implemented and contained in the code base. A practical theory of monetary stability in that context is code.

January, 2019

Acknowledgements

I thank Martin Kolmar, Justus Inhoffen, and Christoph Siemroth for comments on earlier and different drafts. I am most grateful for many discussions with Neil Ghani, Jules Hedges, Paulo Oliva, Evguenia Shprits, and most importantly Viktor Winschel.