Programming language for algorithms in laws

[lpetrich]

Programming Language Converts Laws Into 'Provably Correct' Computer Code | Discover Magazine
"Some legal text is so highly prescribed that it functions like an algorithm. So a team of computer scientist have created a programming language that can capture and execute these laws."

... 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.

Many algorithms are very awkward to express in natural language, and that is why mathematical notations and programming languages have been invented.

There have been some efforts to create programming languages with some resemblance to natural language, to make them easier to understand by non-programmers. The most notable effort may be COBOL, one of the first high-level programming languages.

One has in it:
add A to B giving C

But a few years after the first release, someone added into the language some syntax more typical of high-level languages:
compute C = A + B

Will Catala contain anything comparable?

 

[lpetrich]

Catala - "Catala is a domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts."

Like this:

Section 132 - (c) Qualified employee discount defined - (1) Qualified employee discount

The term “qualified employee discount” means any employee discount with respect to qualified property or services to the extent such discount does not exceed—

(A) in the case of property, the gross profit percentage of the price at which the property is being offered by the employer to customers
./section_132.catala_en
/*
scope QualifiedEmployeeDiscount :
definition qualified_employee_discount
under condition is_property consequence
equals
if employee_discount >$
customer_price ×$ gross_profit_percentage
then customer_price ×$ gross_profit_percentage
else employee_discount
*/

At GitHub:
CatalaLang/catala: Programming language for literate programming law specification

 

[lpetrich]

[2103.03198] Catala: A Programming Language for the Law at arxiv

Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm. Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal language leaves corner cases unaddressed. We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant. We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem.

The examples so far are mainly proof of context. Will Catala source code or something similar eventually find its way into statutes and court decisions and the like?

 

[steve_bank]

When I was working at a Lockheed division I had to contribute to a proposal that had a set of complcated contractural interlocking requirements. In one case I ended up putting it into symbolic logic to make sure I had everything covered.