Catala

Automated decision-makingLegislation: executionLegislation: representation
catala-lang.org
Main research: August 2021

Contents

1. What does it claim to do?
2. Substantiation of claims & potential issues
3. How might the end-user assess effectiveness?
4. What form does it take?
5. Is it currently in use?
6. The creators
7. Jurisdiction
8. License

What does it claim to do?

Catala is a :domain-specific language designed for annotating legislative texts with code that is readable by non-experts. This code is executable and can be compiled into general-purpose programming languages for integration in real-world applications. At present, the main focus of Catala is the translation of French tax legislation into executable code.

Claimed essential features

• Write executable code that faithfully represents legislative rules.
• Combine legal provisions with easy-to-understand software code, in one document.

“Catala is a domain-specific language for deriving faithful-by-construction algorithms from legislative texts.” (Github repository; archived)

“Catala is designed to achieve semantic equivalence with the law itself (its fundamental source of truth).” (About; archived)

“Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.” (Github repository; archived)

Claimed rationale and benefits

• Produce software code that mirrors the law, for use in production applications.
• Resolve subtleties and ambiguities in legislation via software testing.
• Render the effects of laws accessible and intelligible.

“…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” (Merigoux et al., ‘Catala: A Programming Language for the Law’ (2021), p. 1)

Catala is meant for areas of law that “…are algorithms in disguise: the law (roughly) defines a function that produces outcomes based on a set of inputs” (ibid., p. 2)

“…the benefits of formalizing a piece of law are the same as formalizing any piece of critical software: numerous subtleties are resolved, and non-experts are provided with an explicit, transparent executable specification that obviates the need for an expert legal interpretation of implicit semantics” (ibid., p. 9)

“…lawmakers and lawyers are given a formal language that accurately captures their intent and faithfully mirrors the prose; programmers can derive and distribute a canonical implementation, compiled to the programming language of their choice; citizens can audit, understand and evaluate computational parts of the law; and advocacy groups can shed more light on oftentimes obscure, yet essential, parts of civil society.” (ibid., p. 3)

“Catala uses a fully-fledged compiler to bring you the code you need, in the programming language you need. That also include legacy environments used in large organizations.” (Home; archived)

Claimed design choices

• Uses literate programming, combining natural language legal provisions and computer code.
• Uses legally-recognised keywords to aid comprehension by non-programmers.
• Integrates default logic to represent defeasible legal rules and exceptions.
• Catala compiler translates Catala code into general-purpose programming languages for use in production applications.
• Uses formal verification techniques to ensure the software code executes as intended.

“Catala is unique because of its use of a style called literate programming, which sees each line of a legislative style text annotated with a snippet of code. This is of obvious benefit because it allows non-technical experts, such as policy makers and lawyers, to understand the representation of the code in relation to the legislation or rules. This allows Catala programmes to be easily verified and validated.” (About; archived)

“The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.” (Github repository; archived)

“Catala’s unique feature is the possibility to give multiple definitions to the same variable, each definition being conditionned (sic) to a logical guard. If the guard is true, then the definition is applicable. This behavior is adapted to the style in which legal statutes are redacted. In the case of multiple guards being true at the same time, the definition is picked according to a precedence in the definitions that is specified in the source code.” (Formalisation; archived)

“Catala also comprises a compiler, which is a mechanism that allows for code to be translated into a range of programming languages, which improves interoperability. For example, the compiler can generate Javascript for web applications, SAS for economic models and COBOL for legacy environments. Crucially, the translated output will be guaranteed to behave in the same way as the original Catala programme.” (About; archived)

“The language is based on the field of formal methods, which are used in safety-critical domains like avionics or nuclear power plants to ensure that software behaves as expected, given a precise and unambiguous description of the expected behavior.” (About; archived)

“Our surface syntax was designed in collaboration with lawyers, who confirmed that the generous keywords improve readability, thus making Catala easier to understand by legal minds.” (Merigoux et al., ‘Catala: A Programming Language for the Law’ (2021), p. 7)

Top

Substantiation of claims & potential issues

• Depending on the quality of the translation of legal provisions into Catala code, the output might not be legally sound.
• Those coding Catala interpretations of the law may not have the legal authority to conclusively determine the meaning of the rules (since they will usually not be working in a judicial capacity). This could be problematic if they are relied upon as authoritative statements of the law and are assumed to have legal effect.
• Maintaining Catala representations of legal provisions may impose significant overhead due to changing judicial interpretations of (i) the original legal provisions, and (ii) fundamental rights that impact their application.
• The claimed goal of achieving “semantic equivalence with law” assumes all relevant legal meaning can be derived from a single document, which is not the case (see Sources of law).
• There may be a risk that Catala is used to formalise areas of law that are necessarily too complex or ambiguous for the kind of deductive reasoning the system is capable of.

Catala is an example of ‘literate programming’, according to which executable code is annotated with comprehensive natural-language descriptions of what is happening (or intended to happen). In Catala this approach is reversed: the descriptions are the legal text, of which the code is a formalisation. That formalisation includes mechanisms to cope with the modularity, flow, recursion, and exceptions present in legislation.

Data

• Initial focus of Catala design has been on French tax legislation, however it can be used for various legal texts.
• Examples of French, Polish and USA legislation can be found here: https://github.com/CatalaLang/catala/tree/master/examples

Catala code

• Writing Catala code is intended to be carried out using a ‘pair programming’ approach, where legal professionals work directly alongside software professionals in order to ensure the translation of legal norms into the Catala language is as exact as possible.

• The literate programming version of the document (‘Catala surface language’) is designed to readable by non-programmers:

Figure 1. US Tax Code §1015(c) in Catala

• The Catala compiler converts this into an intermediary ‘scope’ language from which further versions can be generated (‘transpiled’) in many general-purpose programming languages, ready for integration into real-world systems. Each of these retains the same provable logic as the original Catala ‘human-readable’ code, elements of which can be tested individually with any errors being mapped back to the relevant parts of the legislative text in the ‘surface language’ version.

Figure 2. Catala high-level architecture, taken from Merigoux et al. (2021), p. 21

Resources

• D. Merigoux, N. Chataing, J. Protzenko, ‘Catala: A Programming Language for the Law’ (2021) (provides a proof of the Catala formalisation)

  • Includes formal definitions, design choices, results of proof.

  • User testing: The results of a non-rigorous (n = 18) user test done with IP students at Université Panthéon-Sorbonne regarding the “claim to readability [of Catala code] by lawyers” imply good results (ibid. p. 23 et seq).

• D. Merigoux, R. Monat, C. Gaie, ‘Étude formelle de l’implémentation du code des impôts’ JFLA 2020 - 31ème Journées Francophones des Langages Applicatifs (Jan 2020, Gruissan, France)

• D. Merigoux, R. Monat, J. Protzenko, ‘A Modern Compiler for the French Tax Code’ CC ‘21: 30th ACM SIGPLAN International Conference on Compiler Construction (Mar 2021, Virtual, South Korea), pp.71-82

• S. Lawsky, ‘A Logic for Statutes’ (2017) Florida Tax Review (On the default logic that Catala aims to implement)

Other technical resources

• Syntax cheatsheet: https://raw.githubusercontent.com/CatalaLang/catala/master/doc/syntax/syntax.pdf

• On the compiler pipeline: https://catala-lang.org/ocaml_docs/catala/index.html

• The tutorial gives a run-through of the process of “annotating a legislative text” using Catala: https://catala-lang.org/en/examples/tutorial

Code: https://github.com/CatalaLang/catala

• Examples at https://github.com/CatalaLang/catala/tree/master/examples (FR succession, FR social security, FR tax code, US tax code, PL tax, Hawaii Motor and Other Vehicles (Title 17)

• Test suite (unit testing): https://github.com/CatalaLang/catala/blob/master/tests/README.md

Top

How might the end-user assess effectiveness?

Verification of the Catala compiler: “We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F★ proof assistant” (Merigoux et al., ‘Catala: A Programming Language for the Law’ (2021), p. 11 et seq). The language and the internal type system allow the coders to write examples (test-cases), such that the code does not produce software that behaves differently from the intended translation. The analysis in the paper is very technical, however, so potentially inappropriate for end-users.

The output (i.e. monetary calculation) of a Catala formalisation of part of the French family benefits law was the same as that produced by the state’s official online calculator (Merigoux et al., ‘Catala: A Programming Language for the Law’ (2021), pp. 25-26; online demo at https://catala-lang.org/en/examples)

The results of user testing, mentioned above, could have a bearing on the assessment of Catala’s claims – particularly insofar as these relate to its interpretability by non-programmers.

Top

What form does it take?

Form

Component, Proof-of-concept

Details

Component

It’s a programming language that is used to write (‘annotate’) a version of a real piece of legislation, those annotations becoming executable. This in turn is integrated into some other system via outputs compiled into a subsequent general-purpose language.

Combination

The formalisation of the language is ‘off the shelf’, but by itself this does nothing – bespoke code must be written to reflect an existing piece of legislation – what this is will depend on who is using it and for what.

Top

Is it in current use?

Catala is currently a research project, but it has a great deal of momentum. The utility as a compiler and considering it a ‘language specification’ go hand in hand. However, there currently is no competing Catala compiler; so the interpretation as a compiler makes it easier to interpret as a piece of (running) software.

Top

The creators

Created by

Academics

Details

Project is funded by France’s INRIA, and currently maintained by computer scientists with assistance from legal scholars. The first author of the paper ‘Catala: A Programming Language for the Law’ (2021), Denis Merigoux, has a background in the design and implementation of Domain Specific Languages, and is the core developer of the project.

The Github repository has 15 contributors to the core language, including CS academics but also people from industry and NGOs and others who aren’t identified.

Top

Jurisdiction

Background of developers

Mainly France.

Target jurisdiction

In principle any that has legislation that conforms with the assumptions embedded in the design of the language.

Justification of the formalisation has been mainly derived from US and French legislation, on the assumption of a structure that follows “a general case/exceptions drafting style.” (‘Catala: A Programming Language for the Law’, p. 18)

Target legal domains

So far, Catala has been aimed at tax law, with demos derived from French, Polish, and United States legislation. In principle it is aimed at any legislation that can be represented in defeasible deontic logic.

Top

License

The formalisation and compiler are both open source on Github (https://github.com/CatalaLang/catala), released under the permissive Apache 2.0 license.

Top