说到律政剧，几乎每一集都取决于主观争论和意见的微妙之处。法律本身仅仅是人类戏剧上演的背景。陪审团会倾向于这边还是那边？法律本身并没有给出线索，当然，这也是戏剧的基础。
由此看来，很容易想象法律和那些执行、辩论和挑战它的人类一样不可预测。当然，在某些领域，主观意见起着巨大的作用。
但法律还有另一个截然不同的方面。所谓的计算法学涉及定义明确的概念和通常不需要人类判断的情况。例如，某些领域的税法。“在这些领域，‘法律几乎没有解释的空间，本质上旨在严格描述一种计算、一种决策过程，或者简单地说，一种算法’，”巴黎数字科学与技术国家研究所的 Denis Merigoux 和 Nikolas Chataing 以及美国微软研究院的 Jonathan Protzenko 说道。
计算法学一直是用普通散文起草的，这是一种更适合其他信息的工具，从浪漫诗歌到科学论文。但计算机科学家并不用散文来写算法……那么律师为什么需要呢？
现在，他们不再需要了。Merigoux 和同事们创建了一种名为 Catala 的编程语言，该语言专门用于捕捉和执行法律算法。该团队已经开始将某些法律法规翻译成 Catala，然后进行实现。在这个过程中，他们展示了美国税法如何被翻译成 Catala 代码，甚至还在法国家庭福利的官方实施中发现了一个“bug”，因为法国家庭福利是由一套特别复杂的法规管理的。
法律执行
他们表示，这种法律代码与用散文写成的法律文本相比具有显著优势。其中最重要的一点是，代码的生成方式是可证正确的。因此，它可以透明地执行——例如，用于计算所得税。这应该能增加公众对那些有时隐藏在幕后、涉及大量晦涩、定制代码的系统的信任。
研究人员首先通过翻译美国联邦所得税法第 121 条来展示他们新语言的强大功能。该条款涉及“自用主要居所出售收益的排除”，团队表示这是一个很好的例子，因为“它包含了我们希望用 Catala 解决的每一个困难；并且它是税法中一个被充分研究和理解的部分。”
例如，虽然法规通常向前发展，但它们经常引用需要更新或重新解释的早期定义。“结果更像带有任意跳转和代码重写的汇编，而不是结构化语言，”团队说。
第 121 条具有所有这些特质。它涉及纳税人出售其主要居所但不需要将利润作为收入申报的情况，因此无需对此类利润征税。
第 121 条以以下段落定义了排除条款：
(a) 排除 从出售或交换财产的收益中，不应包含在总收入中，如果在此次出售或交换日期结束的 5 年期间，该财产已被纳税人作为纳税人的主要居所拥有和使用，累计时间达 2 年或以上。
Merigoux 和同事们指出了程序员很容易识别的各种特性。例如，“if”这个词。这设定了排除适用的条件。法规在 (b) 到 (g) 条款中列出了对该排除条款的限制，这些限制引用了一般情况。其逻辑本质上是建立一个默认情况，然后列出例外情况。
所有这些都可以被合适的编程语言捕捉到。Merigoux 和同事们说，这个过程被称为默认逻辑。因此，默认逻辑是他们的新语言 Catala 的基础。“我们已经实现了一个 Catala 编译器，并使用 F★ 证明助手证明了其核心编译步骤的正确性，”Merigoux 和同事们说。
将法规翻译成 Catala 的过程是一个劳动密集型的过程，需要法律专家和计算机程序员之间的密切合作。但这个过程也有助于更好地理解法律文本及其编码的细微之处。
Merigoux 和同事们继续对法国家庭福利法的一部分进行同样的分析，该法以其复杂性而闻名。在此过程中，他们发现法国使用的软件在实施该法律时存在问题，未能捕捉到法律的一些预期细微之处。
代码提取
将法律的本质提取并编码成代码的想法并非全新。各种学者都曾争辩说这应该是可能的，甚至有一两个人尝试过用代码来实现。然而，过去的一个主要障碍是法律和编程社区之间文化差异导致的将法律翻译成代码的困难。
Merigoux 和同事们表示，Catala 至少克服了其中一些问题，并指出它是一个“工业级”工具。“凭借其清晰简洁的语义，我们希望 Catala 法规形式化能够为未来法律的正式分析提供理想的起点，从而能够使用现代形式方法的全部武器来进行法律起草、解释、简化和比较，”他们说。
有趣的工作。但律政剧将再也不同了！
参考：Catala：法律的编程语言：arxiv.org/abs/2103.03198
