Catala

Knowledge Base Software
#1

image
Catala is an open-source programming language designed to allow for “correct-by-construction” encodings of taxation and benefit legislation. This gives enhanced assurances that the encoding of a piece of legislation does not have “bugs”, by making those bugs possible to detect or test for.

It is a functional-style programming language, and legislation encoded in Catala can be compiled into several other languages, including OCaml and Python.

The Catala web page includes tutorials for using Catala to encode legislation in both English and French.

Denis Merigoux's PhD Thesis on Legal Expert Systems
Free Rules as Code Seminar: Lawsky - "Coding the Code: Catala and Computationally Accessible Tax Law"
#2

When I first saw this awhile ago, when I was studying Coq, it was very interesting. It’s essentially bringing a subset of theorem proving to law, allowing it to be more easily used for proving certain properties.

After using Prolog a bit, I wonder, is Catala more suitable than something like Prolog, when most people will want to both ask questions about a law and verify if a certain rule holds?

I believe “literate prolog” can be written and be just as understandable as the Catala examples. It’ll be a fun exercise to do when I get around to it.

#3

Good question.

If you’re interested in literate prolog, you might like to check out s(CASP) + SWI-Prolog = 🔥 | Jason Morris, which uses SWISH.

I haven’t used Catala, yet, so I don’t have any instinct for what using it is like. Practically, it is designed with formal verification front of mind. I don’t think you can say the same thing about Prolog. So I would expect Catala would be better for that.

Also saw a demo yesterday of someone doing it in Lean, which seemed a lot less painful than I would have anticipated. Lean started in the formal verification world, whereas Catala is still trying to add features for it. Lean is general purpose, and Catala is law-specific. Hard to say which is more promising, at this point.

#4

That is the post that precisely brought me here, since it’s at the top of the swi-prolog news page: News .

From what I understand Lean 4 in particular is a very nice upcoming version of the Lean theorem prover. For me though a language which can be understood by the wider population is much useful than the other, even if it’s weaker.

I think formal verification in general has problems when dealing with law and social issues, but I’m not going to put it in the bin just yet. :slight_smile:

Your literate Prolog example is I think a really nice balance between logical deduction and something which can be understood by the average person, given some minimal education. As I said earlier, you can then introduce statistical statements which would just be annoying to encode and verify in a theorem prover.

1 Like