Catala Lang: DSL designed for deriving implementations from legislative texts(catala-lang.org)
catala-lang.org
Catala Lang: DSL designed for deriving implementations from legislative texts
https://catala-lang.org/
44 comments
A healthy dose of skepticism seems certainly warranted. I would like to share an example that I hope illustrates the potential of using programming languages to formalize legal reasoning, or at least one possible usage scenario. Take for instance Article 14 of the Single Digital Gateway Regulation (SDGR), available in its entirety from:
https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=uriserv:...
Article 14 mandates that a technical system be built and states, among other requirements:
"Where competent authorities lawfully issue, in their own Member State and in an electronic format that allows automated exchange, evidence that is relevant for the online procedures referred to in paragraph 1, they shall also make such evidence available to requesting competent authorities from other Member States in an electronic format that allows automated exchange."
The core of this task is therefore to translate evidences between different European Member States. It would be nice to formalize this in the form of logical rules that clearly state which documents can be used to establish the necessary evidences. For instance, the contents of an Austrian birth certificate could be used to prove a required age to a different Member State. The logical rules could take changes in legislation and data formats into account without requiring a redeployment of the entire system, if there is a way to read and interpret the rules dynamically.
https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=uriserv:...
Article 14 mandates that a technical system be built and states, among other requirements:
"Where competent authorities lawfully issue, in their own Member State and in an electronic format that allows automated exchange, evidence that is relevant for the online procedures referred to in paragraph 1, they shall also make such evidence available to requesting competent authorities from other Member States in an electronic format that allows automated exchange."
The core of this task is therefore to translate evidences between different European Member States. It would be nice to formalize this in the form of logical rules that clearly state which documents can be used to establish the necessary evidences. For instance, the contents of an Austrian birth certificate could be used to prove a required age to a different Member State. The logical rules could take changes in legislation and data formats into account without requiring a redeployment of the entire system, if there is a way to read and interpret the rules dynamically.
Thanks for pointing out the broken link, I just fixed it : https://github.com/CatalaLang/catala-website/commit/a5c4157a....
Your question is spot-on; for me the Catala code has to be officially published from the government service that uses it to apply a piece of law automatically with a legal expert system : tax administration, social benefits administration, etc.
If you disagree with the code, then I guess you could sue the administration in court. The legal process for that depends on the country though.
Your question is spot-on; for me the Catala code has to be officially published from the government service that uses it to apply a piece of law automatically with a legal expert system : tax administration, social benefits administration, etc.
If you disagree with the code, then I guess you could sue the administration in court. The legal process for that depends on the country though.
I don't have the references at hand, but I've seen a few rulings now for smart contract disputes along the lines of: "The contract is legal in and of itself, and part of the contract is to be bound to whatever decisions the code makes so long as that decision is itself legal."
The status quo now is that if I have a contract dispute with a big corporation I'm probably SOL as they will bury me under lawyers. But if I can get a summary judgment saying "hey, the code says he's right, pay up BigCo." Suddenly the courts are a lot more accessible to me.
Not saying this will be a net win for the little man (automation usually isn't) but there may be some benefits, which is interesting.
The status quo now is that if I have a contract dispute with a big corporation I'm probably SOL as they will bury me under lawyers. But if I can get a summary judgment saying "hey, the code says he's right, pay up BigCo." Suddenly the courts are a lot more accessible to me.
Not saying this will be a net win for the little man (automation usually isn't) but there may be some benefits, which is interesting.
it has to chain back to reality eventually though.
the courts have had to rule over whether action figures are toys or dolls, because those had different tariffs: https://en.wikipedia.org/wiki/Toy_Biz,_Inc._v._United_States
you can make an incredibly verbose smart contract but lawyers will weasel about the inputs like this.
the courts have had to rule over whether action figures are toys or dolls, because those had different tariffs: https://en.wikipedia.org/wiki/Toy_Biz,_Inc._v._United_States
you can make an incredibly verbose smart contract but lawyers will weasel about the inputs like this.
Sure, I don't think my post disagrees with that. You're discussing regulation. I only referred to a very particular type of legal case: a contract dispute between two private parties wherein the contract is legally valid and the parties have agreed to abide by the determination of the program.
Not all law will be like this, it's too complicated, but some of it might be and that's interesting.
Not all law will be like this, it's too complicated, but some of it might be and that's interesting.
[deleted]
> I don't think a programming language will benefit law in any capacity.
It sounds like your concept of law is rather static. Don't you think human society will eventually start to create "law" that doesn't follow the traditional model of imprecisely expressed statements, expressed in a weird bastardization of natural language?
It sounds like your concept of law is rather static. Don't you think human society will eventually start to create "law" that doesn't follow the traditional model of imprecisely expressed statements, expressed in a weird bastardization of natural language?
In very specific contexts, computational law can make sense. My company, for example (https://droit.tech/), has had success in the financial regulation space.
Is this something we could use to create whole new legal systems and then convert them into natural language?
Why is it called like the natural language "Català", from Catalunya (or Catalonia), in Spain?
It looks like a mix of a functional language and Prolog.
It is actually a purely functional language : the compiler translates all the code to lambda calculus at some point (https://dl.acm.org/doi/10.1145/3473582).
i found this recently and got really excited about the idea of computational law- but then i looked close and saw that all the examples were complicated tax and benefit accounting rules for the french government and thus rose the tombstone for my interest in computational law.
Yeah this seems boring and uninteresting but you might be surprised to hear that large organizations struggle a lot to get those things right: https://federalnewsnetwork.com/tom-temin-commentary/2020/01/...
not surprised at all! and it is, indeed, critical for the functioning of society. just not something that i traditionally have taken interest in.
i was hoping to see something along the lines of a dsl that improved the precision of how law is expressed in a more general sense, and perhaps tooling for collaborating, patching, managing, diffing and otherwise computerized reasoning about the law that doesn't necessarily supplant a lot of what legislators and the judiciary do, but rather increases the effectiveness with which they are able to do their jobs.
i was hoping to see something along the lines of a dsl that improved the precision of how law is expressed in a more general sense, and perhaps tooling for collaborating, patching, managing, diffing and otherwise computerized reasoning about the law that doesn't necessarily supplant a lot of what legislators and the judiciary do, but rather increases the effectiveness with which they are able to do their jobs.
Aren’t ambiguities in the law usually features rather than bugs?
Only for lawyers to use exploits and backdoors.
Legislators rely on ambiguity and selective enforcement to keep laws simple. For example, the US Controlled Substances Act makes it illegal to possess a controlled substance without a prescription or license. Bufotenin is a controlled substance that also happens to naturally occur in the human body.
Congress won't write an exception to permit the possession of un-extracted naturally occurring quantities of endogenous substances within one's body because they know that the law is not enforced by robots who will automatically arrest everyone in the country. They probably never even gave the concept a passing thought because it's entirely outside the realm of what a judge would ever consider to be reasonable.
Congress won't write an exception to permit the possession of un-extracted naturally occurring quantities of endogenous substances within one's body because they know that the law is not enforced by robots who will automatically arrest everyone in the country. They probably never even gave the concept a passing thought because it's entirely outside the realm of what a judge would ever consider to be reasonable.
It's worth noting that drug laws don't necessarily treat substances as being in your possession once they have been consumed, and although they might criminalize the "use" of drugs, that can require proving intent, which is not necessarily possible to establish solely from the presence of the substances (or their metabolites) in the suspect's blood.
The 1993 case State v. Lowe gives a good explanation of the legal reasoning:
"The absence of proof to evince knowledgeable possession is the key. The drug might have been injected involuntarily, or introduced by artifice, into the defendant's system."
https://www.leagle.com/decision/199383586ohioapp3d7491724
The 1993 case State v. Lowe gives a good explanation of the legal reasoning:
"The absence of proof to evince knowledgeable possession is the key. The drug might have been injected involuntarily, or introduced by artifice, into the defendant's system."
https://www.leagle.com/decision/199383586ohioapp3d7491724
Not to get political, but what about things like gun laws, where some of the definitions are loosely defined and written by morons with no true understanding of the subject matter. How are those going to be translated into hard-and-fast definitions?
On second thought, that applies to many laws, but my question still stands.
On second thought, that applies to many laws, but my question still stands.
Catala is not meant to formalize a law which obviously was not written to "compute" something. It is meant as a tool to improve the fair and just enforcement of pieces of law that effectively define an algorithm that can be enforced by a computerized system.
The process of developing the formalism would actually surface a lot of those issues. The distinction between "pistols" and "rifles", for example, raises many practical questions...
[deleted]
Very interesting! Previous discussions:
https://news.ycombinator.com/item?id=27059899 (5 months ago, 129 comments)
https://news.ycombinator.com/item?id=24948342 (10 months ago, 37 comments)
As I see it, a language intended for use in legal contexts such as contract law and legislation must satisfy two key desiderata:
(1) it must be able to express the intended laws and contracts
(2) it can used to conveniently reason about these rules themselves too.
It is property (2) I miss most when seeing this proposal.
When I undertake the task of formalizing legislation or any type of rules, one of the key benefits I would like to obtain as a result is the ability to answer questions such as: "Are there redundant regulations or clauses?", "Can these conditions be simplified?", "Are these conflicting conditions?" etc. Such questions require reasoning about these rules themselves.
https://news.ycombinator.com/item?id=27059899 (5 months ago, 129 comments)
https://news.ycombinator.com/item?id=24948342 (10 months ago, 37 comments)
As I see it, a language intended for use in legal contexts such as contract law and legislation must satisfy two key desiderata:
(1) it must be able to express the intended laws and contracts
(2) it can used to conveniently reason about these rules themselves too.
It is property (2) I miss most when seeing this proposal.
When I undertake the task of formalizing legislation or any type of rules, one of the key benefits I would like to obtain as a result is the ability to answer questions such as: "Are there redundant regulations or clauses?", "Can these conditions be simplified?", "Are these conflicting conditions?" etc. Such questions require reasoning about these rules themselves.
Hi, Catala author here! (2) is definitely possible since the language has a formalization and is proof-oriented. I have plans to connect it to theorem provers for the kind of application you're referring to, just didn't have the time to do it yet :)
On a side note, I wonder if you've considered the use of a controlled natural language for this.
Im a layman on these topics but I often think an intermediate translation to a controlled natural language should be invaluable (e.g. you can train a NN to translate, and a human can verify it without knowing about coding).
I've considered it, but from interactions with lawyers it seems that you don't need to put that degree of sophistication into the syntax for lawyers to be able to read and review the code. Turns out semantic features like the possibility of splitting the code into base case/exceptions and definitions under condition seem more important.
Catala is just a functional language under the hood, and its syntax is very basic (it has an LR(1) parser) with just verbose keywords.
Catala is just a functional language under the hood, and its syntax is very basic (it has an LR(1) parser) with just verbose keywords.
Thank you a lot for taking the time to respond!
Could you please give a short example of how we can use Catala to interpret for instance the sample program that is shown on the project page? Does it have a natural representation as a Catala data structure that can be reasoned about conveniently within Catala?
Could you please give a short example of how we can use Catala to interpret for instance the sample program that is shown on the project page? Does it have a natural representation as a Catala data structure that can be reasoned about conveniently within Catala?
No, the language does not have self reflection, it is a domain specific language that is not even Turing complete. However Catala programs could be compiled to deep or shallow embeddings inside other programming languages, including inside theorem provers interactive (Coq, F*, Agda, etc.) or automatic (SMT solvers, abstract interpreters). You would then be able to reason about your Catala programs inside these external provers.
Why did you choose the name of an existing language (català, Catalan) for your new language?
I'd like to add that an ideal legal language should end up heavy with definitions. Whether or not a person has performed an action is often an important legal question, even after the a t is clearly defined and the person identified. To this end I think such a language should have some formal definitions of what it literally means for a specified person to perform a specified act.
You could go on for some time defining terms here, and would have to if you want to mechanically determine legal outcomes, once the required quantifiable facts have been established. I think you'd end up with something look like one of the ill-fated expert systems of yesteryear.
You could go on for some time defining terms here, and would have to if you want to mechanically determine legal outcomes, once the required quantifiable facts have been established. I think you'd end up with something look like one of the ill-fated expert systems of yesteryear.
Thanks for the previous discussions ! I've been trying to link catala-lang.org for a couple of months on HN but _never_ envisaged it was already linked from GitHub or papers. :)
Working with Catala in academy. Also trying to model Catala as a type system embedded in Haskell
Hi, Catala author here. This is amazing! Please get in touch if you have any questions or just want to talk :)
[deleted]
Cool idea, I'm sure many programmers have pondered this concept (albeit briefly, in my case).
Found a code sample in the README:
https://github.com/CatalaLang/catala/raw/master/doc/images/S...
Unsolicited feedback: this should be the first or second thing visible on the home page, ideally in a less funky font.
Found a code sample in the README:
https://github.com/CatalaLang/catala/raw/master/doc/images/S...
Unsolicited feedback: this should be the first or second thing visible on the home page, ideally in a less funky font.
I'm very interested in computational law and appreciate all links to people exploring this space. Another I found recently in Singapore: https://cclaw.smu.edu.sg/
If there's a dispute around existing code, who's going to translate it to Catala?
If there's legal reason to write a specific program for something, why wouldn't that be some kind of patent or similar?
The only English example (US Tax Code) has a broken link too, "source code files of the example", so I can't even see that.
Idk. Just doesn't seem useful from what I see so far.