Specification languages for computational laws versus basic legal principles

TL;DR

The paper tackles how to express computational laws for automated decision making, weighing natural language against formal specification languages in the context of the EU road-transport regulation Art. 6.1. Using Regulation 561/2006 and tachograph rules, it analyzes five legal principles—$Legality$, $Legal ext{-}Certainty$, $Prohibition ext{-}of ext{-}Arbitrariness$, $Motivation$, and $Clarity$—to assess benefits and drawbacks of each language. It demonstrates a NL version of Art. 6.1 and a formal Gallina specification, illustrating how formalization enables precise semantics and formal verification while potentially sacrificing accessibility. The core contribution is a structured, principle-by-principle comparison that clarifies trade-offs between interpretability and verifiability, arguing for a balanced or hybrid approach, such as Structured Natural Languages, in developing computational laws. The work has practical implications for policymakers and developers by guiding the design of ADM-compliant regulations and highlighting the importance of formal verification in ensuring correctness and accountability of automated regulatory decisions.

Abstract

We speak of a \textit{computational law} when that law is intended to be enforced by software through an automated decision-making process. As digital technologies evolve to offer more solutions for public administrations, we see an ever-increasing number of computational laws. Traditionally, law is written in natural language. Computational laws, however, suffer various complications when written in natural language, such as underspecification and ambiguity which lead to a diversity of possible interpretations to be made by the coder. These could potentially result into an uneven application of the law. Thus, resorting to formal languages to write computational laws is tempting. However, writing laws in a formal language leads to further complications, for example, incomprehensibility for non-experts, lack of explicit motivation of the decisions made, or difficulties in retrieving the data leading to the outcome. In this paper, we investigate how certain legal principles fare in both scenarios: computational law written in natural language or written in formal language. We use a running example from the European Union's road transport regulation to showcase the tensions arising, and the benefits from each language.