Limiting Inconsistencies in Legal Languages

Inconsistencies play different roles in law and in logic, respectively, and programming languages designed to code law should therefore, when possible, be designed to prevent the encoding of inconsistencies. While inconsistencies in standard logic “explode” the argument, allowing anything at all to be proven, apparent inconsistencies in law simply indicate that further guidance is needed. 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.

This 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 the 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, helps prevent the implementation of certain inconsistencies.