Catala – Law to Code

Catala is specifically for tax codes and other laws that involve formulas and calculations, not all laws, so I don’t think most of your concerns apply to it specifically. There are often complicated rules governing how, e.g. benefits or tax credits are calculated that natural language is clumsy at expressing, so having a formal language that encodes that logic seems useful.

I agree government/justice by algorithm would be very dangerous, but Catala does not seem to be that.

It’s also the case that the massive set of constantly evolving case law is akin to the most convoluted and buggy “libc” ever implemented, running on a system where random bit flips occur frequently. Any lawyer who says they know how to definitively encode an assumption is inherently making a probabilistic statement colored by their own experience and definitionally limited exposure to case law - it may be near perfect, but it exists in an imperfect runtime environment.

This doesn’t mean that this isn’t a useful tool as an aid for interpretability. And perhaps we can reach a point where ambiguity in case law can “propagate” through a graph of nodes to give a range of answers to any question about a regulation - perhaps with the aid of LLMs. But until we have such a system, it can be dangerous to draw conclusions from systems like this one.

(Not a lawyer, this is not legal advice.)

> "interpretations"... which are different from what the law literally says.

We have to remember that the letter and spirit of the law can grow apart over time, and loopholes are often gamed before that naturally happens anyway. So obviously we still need judges to keep the "spiritual" aspect of intent alive, so that evil isn't laundered through technicality.

"Literal" should really be a concrete thing, but it does feel strangely connected to a problem that has existed since Sola Scriptura, up to Gödel's theorem. I think about this everytime software and law collide. That article on "what color are your bits"[1] also comes to mind.

[1]: https://ansuz.sooke.bc.ca/entry/23

Do you really want, for example, the US constitution's write time understandings to be perpetuated forever? Their understanding of "citizen" did not include neither women nor black slaves, just to take one example. Another example is the famous question of "whether or not the right of a woman to abortion is a consitution-guaranteed federal right?" to which a bunch of very important folks gave an answer in 1973 but another bunch of very important folks gave a different answer in 2022.

[dead]

I have a potentially more optimistic (and simultaneously more pessimistic!) view to offer.

Some differing interpretations of the law distinguish between the lawmakers' intention vs the literal meaning (and keep in mind that language itself changes a lot in just a few centuries. The hard problem is that, in PL terms, the law is written in syntax without agreed upon semantics. So a decent step could be just using some agreed upon semantics, like we do in code! Then at least "interpreting" it would be unambiguous.

Maybe a decent analogy would be gcc vs clang might produce different programs for certain undefined behavior, and different combinations of pieces might lead to different behavior too (like race conditions), and somebody (the plaintiff/user) is asking you (the judge/compiler) to decide what's going to happen in this next loop/program/whatever.

Or maybe a decent analogy would be getting a ticket that the API is erroring in some rare user's case and having to look into the code and stacktrace to realize it's some weird unanticipated interaction between two different pieces of legacy code (150 year old law) that now interact due to a recent merge (a new law from last year), and now it's crashing, so we have to figure out how to interpret/compile/resolve this user's case.

If law was usable like code, we'd never have any of those issues, just like we never have those issues with actual literal programs. And when we do, it's just because we're using the wrong language/aren't encoding enough things in the types and semantics/shouldn't have used this niche compiler so now let's get a new interpretation from another Supreme Compiler/etc. Life would be easier \s

So it's maybe more optimistic than you, in that the run/read time power (judicial) doesn't get diminished, but more pessimistic in that I believe it because I believe that changing the language from english law jargon to some formal language doesn't actually eliminate the issues it might be intended to eliminate.

Yes, this would make us programmers so happy wouldn’t it :)

Right, but if laws were developed in regulatory sandboxes, you'd also have the opportunity to red-team them.

Might be a design idea for future lawmakers.

It does stand to reason that all law could be formalized. For example, consider the definition of murder in the first degree from 18 USC § 1111:

"Murder is the unlawful killing of a human being with malice aforethought."

You might say, well, "unlawful" and "malice" are fuzzy concepts; but we can take them to be facts that we input into the model. I guess we could write something like this in Catala:

    scope Murder :
      definition in_the_1st_degree
        under condition is_malice_aforethought and is_unlawful consequence
      equals
        true

In the calculation of social benefits and taxes, the facts input to the model are generally things like prices, depreciations, costs, areas of offices, percentages and so on, input numerically and sworn to be true. These numbers are then used to calculate an amount due (or in arrears). Performing the calculation in a way that is verified to conform to the law is a big part of the work.

However, in other areas of law, determining the facts is actually where the real work is -- was there malice aforethought? A formalized legal machine could process these facts but it's not a big help. The models would just be a huge list of assumptions that have to be input and a minimal calculation that produces `true` or one of the alternatives of an enum.

Law isn't written to cover 100% of real life scenarios and potential cases, it's written with deliberate parts of ambiguity, that will ultimately be up to courts to set the precedents for, in various situations and context.

I think the idea is that you can't really cover 100% of real-life cases in "code", either legal or software, so the areas you'll leave this out of would be those "not-entirely-strict" parts.

A computer program takes digital bytes, runs some discrete logic on them, outputs some more bytes. Laws take messy real world stuff, run some subjective decision tree on them, and output some messy real world actions to take. If you model the former with the latter you end up 'shelling out' to human judgement every 2 words. Suppose you accidentally shoot somebody while duck hunting, the meaning or value of pretty much everything here can't be determined by a computer, so the code-law version of this random snippet of natural-language-law would be pretty useless:

> If it is found that the defendant did the killing or wounding, but that it was not intentional or negligent, the court shall dismiss the proceeding. Otherwise, if it is found that the defendant did the killing or wounding intentionally, by an act of gross negligence, or while under the influence of alcohol, the court shall issue an order permanently prohibiting the defendant from taking any bird or mammal.

A lot of law is based around subjective gray lines. “How would a reasonable person behave in this unique situation?” Is at the root of a lot of legal situations.

Write a function for that, keeping in mind that “this situation” needs to be modeled with potentially infinite variables. Then try to define a “reasonable person”.

Hell, the reason most trials happen is because there is huge grey area, and the written laws are not obvious as to what the outcome should be.

Commercial law nuts and bolts is very algorithmic often.

Criminal law is often fundamentally subjective, incorporating questions of intent and remorse.

I assume it would fail to compile, or error out, because of myriad conflicts throughout the body of laws.

I think the primary reason is that laws are about human convention, not real objects which one can clearly and deliberately define. Like at the most basic level nothing exists at all except for quantum fields or something like that. Everything else we talk about on a regular basis, people, dogs, streets, businesses, etc, is defined by convention to a greater or lesser degree.

It is therefore quite hard to create a formal system to refer to objects in the world in a way which induces no contradictions with intuition. This is why we have courts, among other functions of government.

Basically, all human knowledge is an application of either math or philosophy, and law is philosophy, so cant be modeled by math

Sure - just add an AI and money will flow.

Yeah, I speak Catalan, and we call the language "català" in Catalan, I mean, I would say "Jo parlo català" to say "I speak Catalan".

I agree that maybe do a quick Google search would avoid this strange appropiation.

That's not so important in Napoleonic/Civil jurisdictions like France. Judges can consider prior rulings, but the law as-written is the main thing.

Not even unrelated, Catala (the law-language) seems to be a French project, supported by institutions in France, and Catalan seems to have a intertwined history with France: https://en.wikipedia.org/wiki/Catalan_language#France

Catala != Catalan