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.
翻译:总的来说,法律是现代社会的基础,对公民日常生活的许多方面进行编纂和规范。法律往往受到各种法院和司法管辖区的解释、辩论和质疑。但在其他一些领域,法律几乎没有什么解释的余地,基本上是为了严格描述计算、决定程序或简言之算法。不幸的是,编稿仍是一个极为不足的工作工具。缺乏正规主义使工作变得模糊不清;法律法规结构,许多段落和分节分布在多个网页上,使得难以计算某一文本所根据的算法的预期结果;而且,正如任何其他定义差强人意的关键软件一样,使用非正规语言使转角案件得不到解决。我们引入了Catala,这是我们专门设计用来允许将成文法简单和系统翻译为可执行的新的编程语言。Catala的目的是通过一个共同的媒介将律师和编程集中在一起,他们能够理解、编辑和演变,弥补常常导致法律执行严重错误的空白。我们为Catala编译了一个编程,并且像任何其他关键软件一样,我们用一个更准确的编程,我们用一个更精确的编程来编程,我们用一个更精确的编程来编程来编程,我们用一个更精确的编程,我们用一个精度来编程来编程,我们用一个精细的算。