Limiting Inconsistencies in Legal Languages
12 March 2024This talk is based on a article:
Abstract: Inconsistencies and contradictions play drastically different roles in law and in logic, respectively, and programming languages designed to code law should therefore, to the extent possible, be designed to prevent the encoding of inconsistencies. Programming languages should be limited not because such inconsistencies do not exist in the statute, but rather exactly because they do. Inconsistencies in the law should, as they are now, be addressed by Congress, the courts, and administrative agencies, and any computer code implementing the law should represent the law as detangled by the relevant branch of government. The article provides an example of a tax statute that mandates inconsistent outcomes for the same set of facts and shows how that inconsistency has been addressed by Treasury and the IRS. The article establishes the inconsistency in part by using an automated theorem prover. The article also shows how a particular domain-specific programming language, Catala, prevents the implementation of certain inconsistencies.
