Euclides algorithm. Source: Wikipedia

Euclides algorithm. Source: Wikipedia

In the VOTEID conference held in Switzerland in 2015, some mathematicians presented a paper where they explained how the tally method used in the state of Tasmania (Australia) works with a Single Transferable Vote (STV) system as specified step by step in the law, but the law is written with ambiguity and part of it was subject to interpretation. STV is quite complex, so the tally is currently done by a company that has created the software that computes the tally. It turns out that the company of course had to implement the ambiguities in the law of the STV algorithm in a specific manner, but the specific way those interpretable parts of law were being resolved is obscure and not public.

These mathematicians had taken the time to reformulate mathematically the tally system as closely as possible to as it was defined in the law, translating it from english to formal logic statements. Then they implemented the tally procedure as a computer program that could be verified to match with those formal logic statements. Finally, they had also worked with the government to propose some modifications in the wording of the law to resolve its ambiguity.

Imagine that you could know and separate what part of a law or regulation can be interpreted, and what part of it is crisp and not subject to different interpretations. Imagine that you could know what the law says about any topic instantly, without needing the help of a lawyer or a legal precedent. Imagine that you could independently know whether a norm is compatible or not with another norm.

Those are some of the promises of machine executable legal code. Having any given normative available in a machine executable format allows you to input the specifics of a case as facts, and the algorithmic legislation would return the decision based on the case, much like a judge would do, without the arbitrary nature of a human judge and in a matter of milliseconds.

Let’s take an example law of a normative in plain english:

The maximum allowed speed of a vehicle on the highway is 120km/h. In case of exceeding more than 50% of the maximum speed limit, the fine will be 900€, otherwise the fine will be 300€.

There are multiple problems with the previous example regulation:
– It’s written in an inexact, ambiguous, interpretable, natural language. Even the same word can have multiple conflicting meanings in any natural language.
– The correctness of a law written in natural language has to be checked manually by humans, which is not an infallible procedure. That creates loopholes in the laws. Our example regulation doesn’t make it clear who will be charged, the driver or the owner of the vehicle.

The same legalese can be expressed in machine executable legal code expressed in the Scala programming language:

With machine executable legal code, there is a clear separation between what part of the law has no margin for different interpretations (the code, the algorithm) and what part of it is subject to interpretations (the input values of the algorithm). This might seem simple, but it is a quite powerful change.

Anyone can execute the law with different input values. For example you can go to this page to test what would be the fine for John Doe if he was driving a vehicle at 190km/h on the highway. You don’t need a law or a judge to play with different input values and check the certain result of each of them; any computer can calculate it in a split of a second.

This doesn’t mean that the interpretation of the law is automatic and instant; reality is never that easy. It means that you can reduce the interpretable and ambiguous part of the law as much as possible, and the machine executable becomes trivially and instantly transparent, accessible, deterministic, technical. Just like any open source software.

The effort of formulating laws in mathematical language must not be underestimated. On the other hand, this can be seen as an investment: the time, resources and money that it would save are yet to be analyzed deeply, but could potentially pay off. Typical software quality techniques could be applied too: unit testing to detect bugs and regressions, integrity tests to detect collisions with other laws. If law becomes software, lawyers become programmers and good lawyers find ways to use the law in unexpected ways, just like good computer hackers do. Society uses laws just like they use software, and the judicial power dictaminates if the software was correctly executed or not.

There are already some steps taken in this direction. Machine executable legal code is not, but machine readable legal code is already quite comon. This means that the law is encoded in a format that a machine can easily read, but not execute. The governments of the United Kingdom, the Netherlands and United States already publish their laws in this manner. The idea of machine executable regulation is being explored by blockchain community through what they call smart contracts.

Machine executable legal code is of interest in the field of electronic voting because it is a matter subject to regulation, as we saw at the beginning of this article. In high-stakes elections at nVotes we setup an Action Protocol with the different parties involved in an election, an emergency protocol where we specify what should be done by what party in which emergency case. One of our R+D projects involves translating these protocols from natural language to machine executable legal code, automating the execution of the protocols as much as possible, reducing to the bare minimum the possible human error and the time needed to execute them, therefore increasing efficency and reducing the operating costs.