Catala：一种用于法律的程序设计语言
Catala: A Programming Language for the Law
摘要：
法律是现代社会的基础，规范和管理公民日常生活的许多方面。通常，法律在不同的法院和司法管辖区受到解释、辩论和质疑。但在其他一些领域，法律几乎没有留下解释的空间，基本上旨在严格描述计算，决策过程或简单地说，算法。不幸的是，散文仍然是一个可悲的不足的工具的工作。缺乏形式主义为模棱两可留下了空间;法律法规的结构，许多段落和子章节分布在多个页面上，使得很难计算给定文本背后的算法的预期结果;而且，与任何其他缺乏具体说明的关键软件一样，非正式语言的使用使角落的情况无法解决。我们介绍Catala，这是一种新的程序设计语言，我们专门设计用于将成文法直接和系统地翻译成可执行的实现。Catala旨在通过一个共享的媒介将律师和程序员聚集在一起，他们可以一起理解，编辑和发展，弥合经常导致法律严重错误实施的差距。我们已经实现了一个编译器的Catala，并证明了其核心编译步骤的正确性，使用F* 证明助手。我们在几个伪装成算法的法律文本上评估Catala，特别是美国联邦所得税第121条和拜占庭式的法国家庭福利;在这样做的过程中，我们发现了官方实施中的一个错误。我们观察到，作为正式化过程的结果，使用Catala使律师和程序员之间的丰富互动，从而更好地理解最初的立法意图，同时产生一个正确的结构可执行规范可重用的更大的软件生态系统。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
