Catala: A Programming Language for the Law
arxiv.org
arxiv.org
It's already the case in many countries today that there is too much focus on the wording of the law and not enough on the intent. People try to use a rigid fixation on the importance of words to twist the law in any direction which benefits them, even in ways that don't feel right.
We risk a Kafkaesque situation.
Most people today don't write code for safety critical systems. The abstract mentions they already uncovered a "bug" in an active law by rewriting it in their language, so it could be an immensely helpful tool for finding edge cases and loopholes in that mess.
> It's already the case in many countries today that there is too much focus on the wording of the law and not enough on the intent
Again, as the abstract mentions this is intended for laws that are meant to be interpreted 100% literally like an algorithm. Those exist and those are also exactly the ones that should be absolutely consistent.
The real problem I see is that clear, loophole-free laws are often not in the interest of the lawmakers. You only need to take a look at the underhanded ways various parties are trying to undermine privacy.
The fact that a law is internally consistent and free of loopholes does not necessarily mean that it is a good law but an algorithmic approach to creating such laws risks making their creation too easy so that we end up with a large body of law that can't be argued against because it has been 'proven' correct.
I'm reminded of a remark that Donald Knuth made regarding a piece of code. It went something like this: "Be careful if you use this, I have merely proven it correct but not tried to run it."
> Most people today don't write code for safety critical systems. The abstract mentions they already uncovered a "bug" in an active law by rewriting it in their language, so it could be an immensely helpful tool for finding edge cases and loopholes in that mess.
I'll give you an example from a field that I (unfortunately) have a reasonable amount of experience of where the law and contracts are supposed to be interpreted 100% literally like an algorithm: structured finance (eg the subject matter of the 2008 financial crisis). The prospectus of a structured security like a mortgage bond is typically a hundred or more pages of very dense legalese that was worked on intensively by highly-specialised lawyers and bankers for months. Its intent is to set up a small special-purpose company with strict rules on how it operates down to the last penny and zero discretion. This allows investors (in theory) to understand how the bond will perform.
The opening chapter of my introductory textbook on structured credit analysis says the author (who has been part of those teams for years and has worked on hundreds or possibly thousands of bonds) has never read a bond prospectus for a structured security that does not contain serious drafting errors. I personally worked on a bond for months and read, edited and commented on the bond model and prospectus hundreds of times. We certainly were trying to make our prospectus as simple, clear and loophole-free as possible. Then a few years after it launched we discovered we had made a big mistake in drafting it that had gone unnoticed by me, the expert bankers and lawyers and all the investors so far. Luckily we were able to fix the problem without negative consequences. There is literally no chance that this error would have been found or solved by a formal system and if anything it would actually have been worse.
Some things are complex enough that they are just very hard to do. The existing system allows for that by having a rigorous process of dispute, interpretation and argument to decide complex questions post facto.
Maybe I'm wrong, but I don't know how decentralization would change anything other than adding safeties against manipulation if done right.
There is no chance that a formal system wouldn't have revealed this bug? Static analysis and simulations wouldn't have helped?
I agree with this wholeheartedly. Engineers have the ability to automate some very complex issues. But there will always be a class of issues beyond automation, simulation, analysis, etc. and we just have to accept that the only way to solve them is with slow, hard, error-prone work.
It's a fancy new thing that will be branded as helping to avoid mistakes, reduce legal system costs, increase consistency, etc.
So, it will be applied to existing laws more generally than the abstract suggests it should be.
New laws will be made with this in mind, increasing application regardless of whether the new laws are actually literally interpretable.
It will become entrenched and hard to remove as allocated funds to pay people to do the same jobs disappear.
> After close inspection of the OpenFisca code, a discrepancy was located with the Catala implementation. Indeed, according to article L755-12 of the Social Security Code, the income cap for the family benefits does not apply in overseas territories with single-child families. This subtlety was not taken into account by OpenFisca, and was fixed after its disclosure by the authors.
Here's the pull request for their fix to the benefits simulator: https://github.com/openfisca/openfisca-france/issues/1426
Yeah, we crossed that Rubicon like Evil Kenevil jumped the Grand Canyon a long time ago.
I'd like to see this sort of rigor applied to the tax code so that we can all agree that "complexity is a subsidy" and just scuttle the whole mess in favor of something not an iron rod of oppression.
> it would be better [to adopt a law system] which maximizes the human interpretive element rather than attempts to remove it.
> twist the law in any direction which benefits them, even in ways that don't feel right.
The first statement seems to say that the more humans can interpret the law the better, the second statement seems to imply that people actually doing such interpretation with the tools available now is a bad thing.
It's a good thing your comment is not a legal text though. Otherwise some formalism would be quite welcome to derive the intended meaning.
It's the fact that people have accepted the primacy of the written word that they allow themselves to be swayed to accept verdicts which don't make sense. It's important to factor in the fact that criminal justice involves multiple jurors, so you don't want some outdated wording written in the 1900s to allow one bad juror to use wording of a law or precedent to convince other jurors of a conclusion which best matches the wording but defies common sense.
It's like in the US constitution, there is this paragraph:
”No State shall enter into any Treaty, Alliance, or Confederation; grant Letters of Marque and Reprisal; coin Money; emit Bills of Credit; make any Thing but gold and silver Coin a Tender in Payment of Debts"
And yet today the US government (which is clearly an alliance of states) pays back its debts by printing more money not backed by gold. People have used the wording "No state" to imply that the Federal government is not a state and therefore, it doesn't apply. But clearly this defies common sense about the intent of the law which was to prevent the government from printing unlimited money not tethered to any scarce asset to inflate away its true debt... And yet this is exactly what the federal government (the alliance of states) is doing nowadays.
How does anyone know they got away with a crime if their cases never went to trial? Isn't that exactly what a trial is there to establish.
The USA has a long history of village folk "just knowing" that an accused is guilty. Seldom worked out well.
Pilots have procedures they must follow. So do cops. They just need to do their jobs properly.
Based on probability, you can safely assume that some percentage of them were guilty. That is more correct than assuming that they were all innocent. But to presume innocence simply on the basis that they were not convicted is itself part of the problem wereby the procedure and the wording takes precedence over the intent.
In reality, there is no certainty; some guilty people will be acquitted and some innocent people will be charged. To put too much weight on the words 'guilty' or 'innocent' is to ignore this reality.
The intent of US law is specifically to allow many guilty people to be freed due to procedural errors, and so the fact that this happens is not taking "precedence over the intent".
Also, in the US, no one is ever found "innocent" in court. They are found either guilty or not guilty.
Unless the intent is "it is better a hundred guilty persons should escape than one innocent person should suffer."
in a document delineating what qualifies as states and what qualifies as the federal government with all sorts of text about relations between the two it would seem to be a really reasonable implication to make.
Furthermore your example is in a paragraph that starts "No State shall enter into any Treaty, Alliance, or Confederation", by your logic it follows that the Federal Government cannot ever enter into any Treaty, Alliance, or Confederation because the Federal Government is after all a State.
If those definitions were tacked on afterwards, then it would exemplify exactly the kinds of distortions I'm referring to. I don't know the order in which the US constitution was written but that definitely should affect the intent.
>> Furthermore your example is in a paragraph that starts "No State shall enter into any Treaty, Alliance, or Confederation"
TBH, I didn't even see this interpretation. I guess some people are focused on the wording to an entirely different level. I used the semicolons to interpret it as "no alliance pertaining to the payment of debt" based on my interpretation, it doesn't say anything about alliances pertaining to other matters.
But this seems to reinforce my point. The words can be ambiguous but it doesn't mean we should disqualify the intent altogether.
The reason for the writing of the Constitution was the Articles of Confederation https://en.wikipedia.org/wiki/Articles_of_Confederation being rather problematic for running a nation.
In fact for any judge familiar with the Articles of Confederation and the history thereof, which I would hope was every judge, the interpretation of the paragraph you cite would be completely obvious and pertaining only to the states, because some of the original problems between the states that caused the Constitution to be written was states doing such things as entering into treaties with foreign nations, coining their own money (making trade between states more difficult than needed), etc. etc.
Basically the paragraph is saying "all the stuff you guys were doing or maybe thinking about doing, stops now!" - I say "maybe thinking about doing" because unsure about letters of Marque although I could certainly see it having been done by some of the more haughty states at the time - say New York or Virginia.
Your fact " I read that many criminals in the US get away with crimes because of failures of procedure by the prosecution for example;"
which you interpret as
"this is a clear sign that there is too much focus on the wording of the law. "
could also be interpreted as:
police often use illegal means to target people and fabricate evidence, and the US's well-functioning legal system stops this.
That's not correct: The "alliance of states" was under the (superseded) Articles of Confederation — the governance failures of which led to the 1787 constitutional convention. In contrast, the very first words of the Constitution state explicitly that "We, the People of the United States" [emphasis added] were joining together to establish a national polity that transcended the states.
> People have used the wording "No state" to imply that the Federal government is not a state
It's far, far more than just a mere implication — it's a foundational assumption. See, for example, the Supremacy Clause of the Constitution. [0]
At this point, I want to point out that while a lot of discussion always surrounds the status and the individual rights of the states, I think it really is clear that the US is the state (as in nation) and the individual states, while they have some autonomy, are the inseparable parts that the US is made of, just like in other federal states (nations).
From that perspective, I think the justification for the paragraph you mention is clear: The states are not independent, and therefore they can't have diplomatic ties with other nations. In diplomacy, this has always been the case: Diplomatic ties always exist between independent nations, never between an independent nation and a federal, dependent state. There is nothing like an "Embassy of the U.S. State of Texas to the United Mexican States" since the State of Texas can't have diplomatic ties on its own.
What you mention regarding printing more money does not apply here: The paragraph you mention talks about the US states, but not about the (nation) state itself, the USA. There exists no alliance of states, rather there is a federal republic consisting of states (which in turn are not allowed to have any diplomatic ties of their own). The (nation) state represented by the US government is obviously not a (federal) state inside the US, that would be absurd.
One person's "technicality" is another person's last hope to have a core principle enforced like "innocent until proven guilty".
Intent is a squishy thing that's open to endless subjectivity and biases. Intent should only be used when the letter of the law isn't sufficiently clear.
Separation of Powers was one of the most brilliant concepts undergirding the US Constitution. It's already been damaged pretty badly over the years. We don't need to double down on that damage by insisting upon having judges ignore the wording of laws so they can go with their feelings regarding intent.
Upthread there was a discussion of hundreds of pages going into something as trivially straightforward as the requirements of a financial contract. For something involving human behavior, there will always be billions of corner cases, exceptions, confounding events, and other factors leaving decisions open to a judgment call.
That's why lawyers spend years just learning to read the law, and then reading and synthesizing thousands of decisions that try to patch together all those inconsistencies and gaps. And even then, every case ultimately comes down to a judge's judgment call on which lawyer has done so more successfully... or worse, a jury of twelve people deliberately selected for their ignorance of the law.
Human beings are too squishy to write genuinely precise laws. Lawyers try to pretend otherwise, and that pretension is fundamental to trying to actually have a society. But let's not kid ourselves into thinking that any law is actually rigorous in a sense that a computer programmer, scientist, or logician would recognize.
That is a really, really strained interpretation of this clause. Because these exact words are used to give these powers to other entities in government:
Article I, Section 8, clause 5: [The Congress shall have Power] To coin Money, regulate the Value thereof, and of foreign Coin, and fix the Standard of Weights and Measures;
Article I, Section 8, clause 11: [The Congress shall have Power] To declare War, grant Letters of Marque and Reprisal, and make Rules concerning Captures on Land and Water;
Article II, Section 1, clause 2: [The President] shall have Power, by and with the Advice and Consent of the Senate, to make Treaties, provided two thirds of the Senators present concur
Some of the other things forbidden with "No State" are also expressly forbidden to Congress itself. How is it common sense that "No state" also includes "the federal government" when the federal government is sometimes given the power which is allotted to "no state" and sometimes expressly forbidden as well that which is allotted to "no state"?
If you follow the exact wording of the law, it's easier to find loopholes (like a hacker looking for a breach).
If you follow the intent of the law, then it's much harder. A judge will see if you acted in bad faith, if your actions are against the spirit of the law.
Seek death penalty? Abort, Retry, Fail?_
When trying to compare the legal systems of various countries, it is instructive to note that they differ by large amounts. The basics of Law, and the governing principles and assumptions behind Law, vary quite a lot. Even within countries, the law is often not the same everywhere. Wikipedia has a good map of the 'basic' law systems used throughout the world:
https://en.wikipedia.org/wiki/List_of_national_legal_systems
Writing code is not a single activity, it is a modern means of communication and information transmission. Code is written for a vast range of purposes, some better suited to less rigorous programmers than others. No-one is asking or expecting the authors of bad code that you have in mind to formalize legal systems. The latter task will be on the rigorous side of programming, presumably leaning heavily on static type checking / automated theorem proving.
A friend recently told me "I never needed a lawyer because someone did not understand a contract, but several times because someone tried to finagle with legal sophistry".
I don't want to be too critical, though, it probably can't hurt to work on something new without dragging along all the baggage of the past. Still, it feels a bit strange from an academic perspective.
Ignoring a century of relevant research is not a recommended scientific approach though. The "baggage of the past" are rather the "shoulders of giants".
1 scope Section121SinglePerson:
2 rule requirements_ownership_met under condition
3 aggregate_periods_from_last_five_years of personal.property_ownership >=^ 730 day
4 consequence fulfilled
This probably won't cause a legal revolution tomorrow, but I hope it can be the start of a slow reform toward linguistic precision and machine-friendliness in legislation in the future.
Also it's a bad name, since that's already the (local) name of a widely spoken natural language.
"The language is named after Pierre Catala, a professor of law who pionneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre d’études et de traitement de l’information juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation."
I'm wondering what could result of the combination of smart contracts on a blockchain and this legal language.
Of course nowadays people's names are mostly just symbolic, and you can move to England and still be called Johnny English.
(In fact, as a sibling comment notes, maybe SQL is named after him.)
This depends on the language. In Spanish (and by extension every romance language) no one would know the meaning of Alvarado (they would associate it with the name Álvaro, but just that) or González, but it would be awful to have a name like "Marcos Café/Marrón" (Marcus Brown) or "Carlos Panadero" (Carlos Baker).
I take your point that the origins of surnames in Spain are typically unlike those in e.g. England, but there are plenty of common apellidos originating in physical descriptions, (far away) place of origin, or livelihood.
Software is an axiomatic system. Human behavior is NOT.
From what I've seen, formal methods for legal systems would take the "facts" of a case as given (assumptions), and deduce legal consequences of those.
I am not aware of any system of law that covers all possible human behavior. Common law systems theoretically could because part of the determination of what is covered is up to the courts, thus when you have a new human behavior it is uncertain if it is covered or not until you take it to court, but in a Napoleonic system the coverage of the law must be explicitly stated.
Thus Napoleonic systems would try for consistent but not complete.
> If x is a good person they can go to heaven. Unless they were born on Feb 29th. The previous restriction is lifted if the year is a prime number. The counting of the year is Julian. The destination of heaven is replaced with hell if at least 5 people are on mars.
As the article shows, exactly existing law is fully of "whoops, you better keep on reading to find that override" situations like the above. Formalization still helps by putting all branching up front rather than with the the moral equivalent of COME FROM statements. And that helps whet there or not "good person", "heaven", and "hell" are well defined.
...The responses to this prreprint make me think no only do HN readers not understand the law, but they don't understand programming well either. :/
As a native Catalan myself I was quite surprised by the title.
Before I'm getting excited I want to know how it will be used in the developing world. E.g. perhaps we'll see an automatic smart-judge that goes from Cellebrite evidence directly to machine based torture and public execution with some blockchain sprinkled-on for good measure. See the latest dystopian piece on how Technology helps the developing world fight crime: https://cpj.org/2021/05/equipped-us-israeli-firms-botswana-p...
Written law itself is also not "enough like natural language that non-law people wouldn't run away at first sight".
The whole thing smacks of false precision to me. It's precise about things that are not legally complex to be precise about in the current system, and the language gives the false impression that it's actually going to be possible to be precise about everything.
Secondly, it feels like it will have a similar drawback to sql[1] in that it seems on the surface to be non-technical, but actually requires significant technical expertise to avoid numerous beartraps and understand anything beyond the very most obvious.
[1] Which was originally intended to be a formal version of natural language understandable to non-technical people (hence the original name SEQUEL "Structured English Query Language")
How is the value of "during the 5-year period ending on the date of the sale or exchange, such property has been owned and used by the taxpayer as the taxpayer’s principal residence for periods aggregating 2 years or more" calculated?
> What does it mean to own a property?
What does it mean to own a property under the non-formalized law?
In the end, it means that if you file a tax return that the tax authorities aren't happy with, you can argue in front of a judge whether you think you own something, and the judge will decide whether you do. Based on this they will decide whether your tax return was valid or not. The technicalities of whether you own something in the eyes of the judge have nothing to do with whether your tax return was based on your reading of the law or on a tool based on this language. Either way you must decide whether you think you own something, and the rest of the computation is based on this decision.
> Does it count if you jointly own a property with someone else?
Search the paper for "joint returns", it quotes both the law and its formalization.
> The whole thing smacks of false precision to me. It's precise about things that are not legally complex to be precise about in the current system
<scratches head> The questions you raised do appear legally complex to me. But also I think you misunderstood the whole problem domain. The law currently spells out an algorithm for computing something. The inputs to this algorithm include questions like "do you legally own stuff". These inputs are outside the specific algorithm spelled out in Section so-and-so. They are similarly outside the specific algorithm spelled out in the computer program.
Trying to pretend it's precise like a computer algorithm is I think a really big problem.
The reason I posed those particular questions is that if you try to make this answer the questions you rapidly approach a level of complexity similar to the existing legal codes and still don't have something that could automatically be evaluated.
Again, I think you're arguing about something that the paper doesn't claim to do. It doesn't claim to formalize "the law" as a whole. It claims to formalize part of a single section of a single statute. That specific statute describes precise rules into which you feed boolean and numeric data, and the application of which rules spits out boolean and numeric data. These rules are written specifically so that they are not ambiguous, so that anyone given the same input data would come to the same output conclusion. That's an algorithm.
What is indeed ambiguous are questions of ownership: Did you own a certain property for two years within a five-year period if for part of that period it was co-owned with a friend who then became your spouse and then later divorced you and got the property? But again, this is not what the paper claims to decide. This is something that the algorithm in the paper, and the algorithm of this specific section of the tax code, takes as input as a boolean flag.
> The reason I posed those particular questions is that if you try to make this answer the questions [...]
But again, you do not try to make this answer these questions. And the paper never claims that it does.
The tool described in the paper does not contain a function like "given THE ENTIRE STATE OF THE REAL WORLD, compute whether I owned such-and-such property for two years in a five-year period". The tool described in the paper only contains a function like "given a boolean flag modeling MY CLAIM to have owned (or not) such-and-such property, compute a number for me".
Your reasoning for having owned (or not) a certain property is not checked by the tool described in the paper. It takes your claim about property ownership as a boolean flag and says "well, if you are really sure that your claim is correct, then your tax liability is such-and-such". It doesn't claim to check whether your claim is correct.
There is a possiblity of automating the mundane, the administrative tasks, which seems like this language is taking a shot at - tax law - or such, but probably in the end we will start transitioning to law that just mentions that the taxes are counted by an algorithm and the algorithm is published on GitHub.
Using software metaphors, I think law has too much responsiblites and we need to decouple some stuff.
Source: I am law student, software engineer.
This type of argument is the same as the people arguing types are bad because they alone don't ensure program correctness. They don't need to. They take care of the boring bits freeing up the mind to think about the interesting parts.
(though I never used MPS)
The problem with the law is interpretation. It is not deterministic and that is because only a small subset of human language is deterministic.
A programming language alone does not solve interpretation (what does this statement mean) and trust (can I trust that THE [because there should only be one] interpretation of this statement has been executed). A programming language (interpretation) and a runtime (trust) are both required.
Now, while using a programming language mildly runs afoul of those same risks, the difference in my mind between a programming language and using lojban (or conlang-o-choice) is that the programming language uses the same vocabulary (plus or minus) just with more rigor in the links between the words. One need not already know "re'azda" is "house" in order to figure out "house.value"
If a man accused the wife of a man of adultery, and the river ordeal proved her innocent, then the man who had accused her must pay one-third of a mina of silver.
So, here is justice at work. If she drowns, she was guilty. If she survives, someone gets 1/3 of a Mina. Ur-Nammu is vague here as to who gets the money. Likely the husband.
How would we code this in Catala? I'll start it, someone else can finish it /g
declaration structure Person:
data id content integer
declaration structure Period:
data start content date
data end content date
declaration structure MarriedCouple:
data marriage_date content date
data husband content Person
data wife content Person
declaration structure AccusationOfAdultery:
data couple1 content MarriedCouple
data accuser content Person
data adultery_date content Period
declaration structure River
data id content integer
declaration structure OrdealByWater:
data subject content Person
data river1 content River
data ordeal_date content Period
declaration scope UrNammuLaw14:
context requirements_met condition
context married_met condition
context accused_while_married_met condition
context tested_by_water_ordeal_met condition
...
Because in the normal case, everything will already be there and only the last part must be written. And then, if someone changes the definition of a "River" then you will immediately see all the laws that are impacted and how they are impacted. Sounds good to me.
1. The above law makes it clear that it is only a man who can accuse the wife of another man of adultery. Your code seems to permit other genders as accusers.
2. Similarly it seems only the wife needed to face the river ordeal. (i.e. every person subject to the river ordeal needs to have a husband) Your code seems to allow the husband to subjected to the river ordeal.
Sorry for nitpicking... it was not to attack your attempt at the code, but the entire idea of formalizing the law in this manner might be very tedious, and less precise in practice than natural language.
[but p.s.] reviewing the laws in wiki, the only instance of a 'female voice' is when a slave girl puts down her mistress (and gets the Sumerian equivalent of soap in mouth). So, putting my Sumerian lawyer hat on, 'context' here implicitly affords 'legal voice' only to men. Women were mute as far as the law was concerned. So a Sumerian AI judge using Catala would have no problem with my code :)
After all, those could benefit programmers too.
- Comparing codifying law vs codifying human language/communication in general I think is very unfair. No doubt law is using the form of human written communication but it has structure and it is meant (at least in principle) to be precise. Even if there is some legislation that goes beyond that structure (honestly interested in seeing a few cases) why would we restrict ourselves from codifying all the rest of the legislation? We can have at least part of our law in an executable form, I can't see a drawback with that.
- Just for fun, let's start thinking about the intersection of law binaries and software licences, oh boy! :D
It's extremely rare, approaching nonexistent, for laws to have a precise, deterministic meaning because the vast majority of human language doesn't either. Here's a good example from CodeX (Stanford Center for Legal Informatics) that assesses an extremely simple law, which contains a surprising amount of ambiguity[0]:
> "One technical problem with Computational Law, familiar to many individual with legal training, is due to the open texture of laws. Consider a municipal regulation stating "No vehicles in the park". On first blush this is fine, but it is really quite problematic. Just what constitutes a vehicle? Is a bicycle a vehicle? What about a skateboard? How about roller skates? What about a baby stroller? A horse? A repair vehicle? For that matter, what is the park? At what altitude does it end? If a helicopter hovers at 10 feet, is that a violation? What if it flies over at 100 feet?
[0] https://law.stanford.edu/2016/01/13/michael-genesereths-comp...
I would love to know what these areas are. There I'd debate around all sorts of seemingly little things in the law, like a definition or a word being singular. On top of that you have "discretion" built in and highly utilized with the judge, cop, and especially the prosecutor.
We already have legal algorithms for sentencing, alimony, child support, etc. These are widely decried as terrible. Why would we want more?
declaration scope Section121Return: context return_data content ReturnType context person1 scope Section121SinglePerson context person2 scope Section121SinglePerson context gain_cap content money
Little about this seems compelling and comes off as self-indulgent. Could you imagine the dread of some poor guy with little to no interest in programming having to learn this?
An AST could help me quickly navigate between paragraphs, and make searching the law easier?!
---
[1]: Just someone, who wants to understand law easier, and not spent years having to study it.
"understand law easier" also in the sense of TLDR law.
And yes, I'm aware of the interpretation aspect of the law, but just give me some easy to understand starting point.
Edit: formatting, formulation
>I'm wondering what could result of the combination of smart contracts on a blockchain and this legal language
Is precisely the wrong way to be thinking about this.
The expectation of Law formalised into code is that the benefit lies from the execution: that if you can provide it with the 'inputs' then the neutral computer will do the 'hard work' of working through the consequences and output a decision.
The other intended hope is that the computer can act as a neutral mediator (presumably why what I quoted above also includes the words 'blockchain' and 'smart contracts') which will come to its conclusions justly and without prejudice. Indeed, if you have an agreed upon system via both parties, then it acts like the spinning table at the beginning of the Temple of Doom - allowing two parties with competing interests to come to an accord without trusting each other.
But it is pretty clear to anyone who has worked within a legal or law enforcement context that this is not usually the bottleneck. Lawyers and Justices are usually intimately familiar with the law, and so much of a trial or a case is working through the establishment of the inputs and any of the logical crunching is normally able to be followed through fairly easily by those present.
There is absolutely a case for tools around the law that may superficially seem similar to the above, but in spirit are the complement: search tools for users to easily find related documents, markup to declare and highlight evidence formally (for human consideration, not machine), editors that can assist with writing up legal documents etc.
Something that would seem to be the same thing, for example, would be to create a data model over the existing law to describe the legal architecture as alluded to in the description of the OP: dependencies, exceptions, related articles etc. However, the purpose of doing this in the OP would be to make this executable. The actually useful thing is a lot more banal - to allow things to be surfaced for human inspection and consideration more quickly and easily. It would be to try to spot contradictions and inconsistencies in the law making stage, not in the law interpretation stage. It would be to spot the impact of making a change to one paragraph beyond just the Act that is being scrutinised.
These things are decidedly unsexy to a technical audience, and don't have that same electric feel of 'solving a problem'. Indeed, many of the biggest advances to be made in Law are to be using de rigeur tools in the tech world (such as version control) in a legal context.
A TED talk that summarises some further points:
Where law is unclear, The drafters of the law were unclear what they wanted or could not agree what they wanted or were unwilling to explicitly state what they wanted.
I don't think we need to rewrite our laws in software friendly language.
We shall soon enough be needing to have law and software hand in hand - the obvious example is the self driving car and trolley problem - a car sees child ahead in the road, and cannot brake in time so must swerve, but swerving will kill the driver (or a old man on the sidewalk).
That must be explicitly coded into the car ahead of time - and that will need to be a regulation / law of the jurisdiction because no car company will just choose.
And so we are presented with the perfect problem - it will demand democratic involvement, it is impossibly hard ethically, and it will need the software to be inspectable / verified before and after the incident.
If we solved those problems then the recent Post Office debacle would have different .
always strikes me as so fundamentally wrong, and also very dangerous.
Goedel's incompleteness theory shows that an axiomatic system can either be consistent or complete, but not both.
Software is an axiomatic system. Human behavoir is NOT.
Law provides remedies for specific harms, such that vengeance becomes the right/duty of the state (which hopefully tempers it with justice)
Law thus needs room for interpretation and for understanding of the human. Thus the need for a judge. Thus a jury. etc.
As one man put it, "the letter of the law kills". Software is only the letter.
We all want clear, black and white guidelines on "good" and "bad". We sometimes look down on religions which seek to provide this.
For the love of $diety$, let's not make software that $diety$
Thus I think any attempt to translate a written law into something a computer can interpret as a failure, because the interpreter is not optional in the law. The interpreter is part of it and constitutes a vital piece of it, and without it written law does not make a lot of sense at all. Still, it is, in my view, a program which can be "executed", just not without a lot of context.
Goedel's theorem is about a specific form of incompleteness.
I think you'd have to provide some additional arguments why the theorem would be relavant in this context.
In other words: I don't think law as a formal system needs all the features that are preconditions for Goedel's theorem.
Similarly: Most proof assistants are very much usable without allowing arbitrary recursion.
It really isn't though. When I write software I have to consider the different interpretations by the OS, browser, etc. and draft accordingly. Ditto for when I draft legal documents and need to consider the different interpretations by opposing counsel, a regulator, etc. As someone who drafts legal documents for humans and writes code for computers I can tell you first-hand the two processes are remarkably similar.