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 :)
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.
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.
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.
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. :)
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:
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.
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.
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.
> 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?
Ok I expressed it wrong. I am just trying to embed a legal DSL it in Haskell and get the type system to help building type-safe contracts - same as embedding the STLC in GADTs
In very specific contexts, computational law can make sense. My company, for example (https://droit.tech/), has had success in the financial regulation space.
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/
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.
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.
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.
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."
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.
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...
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.