Awesome to see someone trying to implement this idea, which I bet most people here have wished existed at some point.
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
Syntax (shown above with line numbers added) looks pretty clean and simple. Hopefully it is enough like natural language that non-techies wouldn't run away at first sight
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.
This snippet begs all the important questions. How is the value of "aggregate_periods_from_last_five_years of personal.property_ownership" calculated? What does it mean to own a property? Does it count if you jointly own a property with someone else? If so, how much of a percentage of ownership counts as ownership? What about if for some part of the 730 days the ownership of the property was subject to dispute and it could have been owned or not owned by the person in question?
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 "aggregate_periods_from_last_five_years of personal.property_ownership" calculated?
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.
The law doesn't specify anything as precise as an algorithm. The law has multiple statutes, codes, precedents etc with overlapping applicability. Then in a particular case these are tried and humans come to a decision.
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.
> The law doesn't specify anything as precise as an algorithm. The law has multiple statutes, codes, precedents etc with overlapping applicability.
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.
Sure, but the problem is then it's not very interesting. There are lots of real-world systems already that do this with existing laws and existing programming languages (eg in the UK where I live the the tax service has a free web filing system where you fill in your tax return online, it checks it for correctness and tells you how much you owe or are owed (if you have overpaid).
Indeed, not the best name, but according to the README, the reason for chosing it was the following:
"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.
Which is a bit circular, because Pierre’s last name is a reference to the region that speaks that language, since he was born in neighboring Occitanie.
The somewhat ironic logic here being that a name referencing a place is very unlikely to come from that place. If Jordi moves from a Catalan area to an Occitan area then he (and his descendants) might be known as "Jordi the Catalan". It wouldn't be very useful to pick that as a name for someone who never left though.
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.)
>Of course nowadays people's names are mostly just symbolic, and you can move to England and still be called Johnny English.
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.
It's a mistake to think that only things which are "absolute" can be logically programing. Take this silly example:
> 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. :/
I agree with this but I also want to see someone try and fail and help us learn from it. This is really one of those untouched territories and there is reward in pursuing that regardless of the end result.
>Software is an axiomatic system. Human behavior is NOT.
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.
I assume you refer to his results regarding axiomatic systems for arithmetic on natural numbers? If a law attempts to capture this, then, sure, it's problematic. But I don't that's very common.
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.
as these things go they will create the illusion of improvement and the chances of things going wrong will be reduced in frequency but when they happen it'll be injustice at cloud-scale. These things have a long fat tail.
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...
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.