The programming language converts legal guidelines into “confirmed appropriate” pc code

When it comes to legal dramas, almost every episode rests on a knife-edge of subjective reasoning and opinion. The law itself is just the backdrop against which the human drama takes place. Will the jury lean in one way or another? The law itself provides no clue which, of course, forms the basis of the drama.

From this evidence, it is easy to imagine that the law is as unpredictable as the irrational people who implement, debate, and question it. In some areas, the subjective opinion certainly plays a major role.

But there is another aspect of the law that is very different. So-called computer law contains well-defined ideas and situations that generally do not require human judgment. For example, certain areas of tax law. In these areas, “the law leaves little room for interpretation and essentially aims to precisely describe a calculation, a decision-making process or, simply put, an algorithm,” said Denis Merigoux and Nikolas Chataing from the National Institute for Research in Digital Science and Technology in Paris, together with Jonathan Protzenko at Microsoft Research in the USA

Computer law has always been written in ordinary prose, a tool better suited to other messages, from romantic poetry to scholarly work. But computer scientists don’t use prose to write algorithms. So why should lawyers?

Now you don’t have to. Merigoux and colleagues developed a programming language called Catala specifically designed for capturing and executing legal algorithms. The team has already started translating certain laws in Catala and then implementing them. In doing so, they show how US tax law can be translated into the Catala Code, and have even found a “mistake” in the official implementation of French family benefits, which is regulated by a particularly complex statute.

Legal execution

They say that this type of code has significant advantages over legal texts written in prose. Last but not least, code can be generated in a demonstrably correct manner. As such, it can be implemented transparently – for example, to calculate income tax. This should increase public confidence in systems that are sometimes invisible and contain lots of lines of obscure, custom code.

The researchers first demonstrate the power of their new language by translating Section 121 of the U.S. Federal Income Tax Act. This deals with “excluding profits from the sale of the primary residence” and is a good example, the team says, because “it has every single difficulty that we want to address with Catala; and it is a well-studied and well-understood part of tax law. “

Although statutes generally evolve, they often refer to earlier definitions that need to be updated or reinterpreted. “The result is more like assembling with arbitrary jumps and rewriting code than a structured language,” says the team.

Section 121 has all of these specifics. It deals with the circumstances in which a taxpayer sells their primary residence but is not required to report the profits as income and therefore does not need to tax those profits.

Section 121 begins by defining the exclusion with the following paragraph:

(a) Exclusion Gross income does not include profit from the sale or exchange of real estate if that property was owned by the taxpayer during the five year period ending on the day of the sale or exchange and was used by the taxpayer as the taxpayer’s primary residence for periods totaling 2 years or more.

Merigoux and colleagues point out several features that are easily recognizable to a programmer. The word “if” for example. This sets a condition when the exclusion applies. The law continues in sections (b) through (g) to list the limitations of this exclusion that apply to the general case. The logic is to essentially set up a standard case and then list the exceptions.

All of this can be captured with a suitable programming language. Merigoux and colleagues say the process necessary to do this is called standard logic. So the standard logic is the basis for your new language, Catala. “We implemented a compiler for Catala and proved the correctness of its core compilation steps using the F ★ Proof Wizard,” says Merigoux and colleagues.

The process of translating statutes in Catala is a labor-intensive process that requires close collaboration between legal professionals and computer programmers. But it is also a process that helps to better understand legal texts and the intricacies they encrypt.

Merigoux and colleagues do the same for part of the French Family Benefits Act, which in its complexity is widely known as labyrinthine. In doing so, they discover a problem with the way this law is implemented in the software used in France, which fails to capture some of the intended intricacies of the law.

Code extraction

The idea that the legal essence of the law can be extracted and codified is not entirely new. Various scholars have argued that it should be possible, and one or two have even tried to implement it in code. However, a major obstacle in the past has been the difficulty of translating laws into codes, partly due to cultural differences between the legal and programming communities.

Merigoux and colleagues say Catala overcomes at least some of these problems, and point out that it is an industrial-grade tool. “With its clear and simple semantics, we hope that Catala formalizations of statutes will provide an ideal starting point for future formal analysis of the law and allow law to be drafted, interpreted, simplified and compared using the full arsenal of modern formal methodology,” say they.

Interesting work. But legal dramas will never be the same!

Reference: Catala: A Programming Language for the Law: arxiv.org/abs/2103.03198