When it comes to legal dramas, almost every episode rests on a knife-edge of subjective argument and opinion. The law itself is merely the backdrop against which the human drama plays out. Will the jury lean this way or that? The law itself provides no clue, which is the basis of the drama, of course.
On this evidence, it’s easy to imagine that the law is just as unpredictable as the irrational humans who implement, debate and challenge it. Certainly, in some areas, subjective opinion plays a huge role.
But there is another aspect of the law that is quite different. So-called computational law involves ideas that are well defined and situations that do not generally require human judgment. For example, certain areas of tax law. In these areas “law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm,” says Denis Merigoux and Nikolas Chataing at the National Institute for Research in Digital Science and Technology in Paris, along with Jonathan Protzenko at Microsoft Research in the U.S.
Computational law has always been drafted in ordinary prose, a tool that is better suited to other messages, from romantic poetry to scientific papers. But computer scientists do not use prose to write algorithms ... so why should lawyers?
Now, they no longer need to. Merigoux and colleagues have created a programming language called Catala that is specifically designed to capture and execute legal algorithms. The team have already begun to translate certain legal statutes into Catala and then to implement them. In the process, they show how U.S. tax law can be translated into Catala code and have even found a “bug” in the official implementation of French family benefits, which is governed by a particularly complex set of statutes.
Legal Execution
They say that this kind of legal code has significant advantages over legal texts written in prose. Not least of these is that code can be produced in a way that is provably correct. As such it can be implemented transparently — to calculate income tax, for example. That should increase public trust in systems that are sometimes hidden from view and involve many lines of obscure, customized code.
The researchers first demonstrate the power of their new language by translating Section 121 of the U.S. federal income tax law. This deals with “Exclusion of gain from sale of principal residence” and is a good example, say the team, because “it features every single difficulty we wish to tackle with Catala; and it is a well-studied and well-understood part of the tax law.”
For example, although statutes generally move forward, they frequently refer back to earlier definitions that need to be updated or reinterpreted. “The result more closely resembles assembly with arbitrary jumps and code rewriting, rather than a structured language,” says the team.
Section 121 has all these idiosyncrasies. It deals with the circumstances in which a taxpayer sells their principal residence but is not required to report the profits as income and so does not need to tax on these profits.
Section 121 begins by defining the exclusion with the following paragraph:
(a) Exclusion Gross income shall not include gain from the sale or exchange of property if, during the 5-year period ending on the date of the sale or exchange, such property has been owned and used by the taxpayer as the taxpayer’s principal residence for periods aggregating 2 years or more.
Merigoux and colleagues point out various features that are easily recognizable to a programmer. The word “if,” for example. This sets up a condition when the exclusion applies. The statute goes on in sections (b) to (g) to list limitations to this exclusion, which refer back to the general case. The logic is to essentially set up a default case and then list the exceptions.
All this can be captured by an appropriate programming language. Merigoux and colleagues say that the process necessary for this is called default logic. So default logic is the foundation for their new language, Catala. “We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F★ proof assistant,” says Merigoux and colleagues.
The process of translating statutes into Catala is a labor-intensive process that requires close cooperation between legal experts and computer programmers. But it is also a process that helps to better understand legal texts and the subtleties they encode.
Merigoux and colleagues go on to do the same for a part of French family benefit law, which is widely known to be labyrinthine in its complexity. In the process, they discover a problem with the way this law is implemented in the software used in France, which does not capture some of the intended subtleties 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 ought to be possible, and one or two have even tried to implement it in code. However, a significant barrier in the past has been the difficulty in translating law into code, partly because of the cultural differences between the legal and programming communities.
Merigoux and colleagues say Catala overcomes at least some of these problems, pointing out that it is an “industrial-grade” tool. “With its clear and simple semantics, we hope for Catala formalizations of statutes to provide ideal starting point for future formal analyses of the law, enabling legal drafting, interpretation, simplification and comparison using the full arsenal of modern formal methods,” they say.
Interesting work. But legal dramas will never be the same!
Reference: Catala: A Programming Language for the Law: arxiv.org/abs/2103.03198
