[denismerigoux]

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

[jhgb]

On a side note, I wonder if you've considered the use of a controlled natural language for this.

[harperlee]

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

[denismerigoux]

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.

[triska]

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?

[denismerigoux]

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.

[grimborg]

Why did you choose the name of an existing language (català, Catalan) for your new language?