denismerigoux

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.

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/...

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).

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.

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.

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.

Hi, Catala author here. This is amazing! Please get in touch if you have any questions or just want to talk :)

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 :)

Very insightful update, I'll remember it. Thanks!

Hi, OP here :) I've come to the same conclusion about programming language creation. However, for a very large organization, it makes sense to have a team in charge of language tooling (see Dropbox/Python, Facebook/Hack/Flow, Apple/Swift). Which is why I'm trying to convince the French state that they should have such a team of permanent people.

Hi, author here :) You seem to be well-informed of the DGFiP jargon, do you know if news of my work has been spreading among the IT department there?

It helps the State and private organizations to comply with the law when computing income tax, payroll taxes, etc. There's a huge gap between the law and how it is applied in some situations https://twitter.com/DMerigoux/status/1304367420639973381

Hi, Catala author here :) Since I'm here please shoot your questions, I'll try to answer them.

Yes it could, although I'm not sure there is a single Prolog system running in production inside a large government agency at the moment.

Also Prolog does not solve all the problems related to programming the law, especially it doesn't have a nice way to handle redefinitions of variables with legislative exceptions as described https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3088206

Hi, Catala author here :) Totally, tax law is usually the most precisely written. But it's still ambiguous as Sarah Lawsky points out https://papers.ssrn.com/sol3/papers.cfm?abstract_id=2987065

Hi, Catala author here :) I totally agree that law should be readable and the Norwegian initiative seems great ! However at least in France we're stuck with the law he have and while some are rightfully proposing some simplification (https://www.revolution-fiscale.fr/), we need a good way to apply the current law faithfully not to end up in situations like this one: https://twitter.com/DMerigoux/status/1304367420639973381.

It's already been tried : http://ceur-ws.org/Vol-2143/paper9.pdf. In a nutshell : NLP techniques don't work so well on the text of law, because it's too messy.