Post

Yeah overall the vast majority of law won’t be usefully provable in this way, only specific things (like tax law) that have highly structured logics. So I bet a lot of admin law? Anyway here is one of the key papers: arxiv.org/abs/2103.03198

arxiv.orgCatala: A Programming Language for the LawLaw 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 ...

1400s: a language is a dialect with a great novel published 1800s: a language is a dialect with an army now: a language is a dialect with a compiler

(I was mostly joking above, but note that if a language is a dialect with a compiler, you have created an automated way of hating people who speak other dialects and that is Bad, Actually)

It’s legit within bounds; basically it only checks a certain subset of English grammar. Which is still a nifty thought experiment!

@chancethelawyer.bsky.social since I see you liked this - have you ever looked at Ken Adams’ “categories of contract language” typology? rigorous checking of that would be a really, really interesting experiment.

Oh, it’s an old one, but the first instantiation I’ve seen in a while, so was fun to trivially play with.