Comment by triska
5 years ago
Very interesting! Previous discussions:
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.
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?
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.
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. :)