Programming language for literate programming law specification
Go to file
2022-07-13 18:40:27 +02:00
.github/workflows check it builds before commiting the modified flake 2022-06-06 11:46:37 +02:00
.nix disable clerk tests in nix build 2022-06-07 08:56:37 +02:00
build_system refactor(clerk): suffix the ninja build outputs with .PHONY instead of .out 2022-07-12 11:16:12 +02:00
compiler Don't print functions on CLI tracing mode; they're too big 2022-07-13 17:27:08 +02:00
doc Added new operator to syntax cheat sheet 2022-06-01 15:23:56 +02:00
examples In the process of debugging AccessionPropriété 2022-07-13 18:40:27 +02:00
french_law feat(backend/ocaml): disambiguate OCaml record names derived from Catala struct 2022-07-12 16:12:18 +02:00
runtimes/python/catala Add mul and div in Python backend 2022-06-01 15:35:55 +02:00
syntax_highlighting Pygments: install as user 2022-05-19 10:40:04 +02:00
tests feat(backend/ocaml): disambiguate OCaml record names derived from Catala struct 2022-07-12 16:12:18 +02:00
.git-blame-ignore-revs Add dune rule to build tests 2022-05-25 18:33:20 +02:00
.gitattributes Remove markdown in github for Catala files 2022-02-16 14:17:40 +01:00
.gitignore Add dune rule to build tests 2022-05-25 18:33:20 +02:00
.ocamlformat Formatting: some other personal preferences 2022-05-11 16:25:49 +02:00
catala.opam refactor(api_web/runtime): runtime_value derive yojson_of 2022-05-25 14:26:58 +02:00
CITATION.cff docs: update the CITATION file 2022-07-07 16:18:08 +02:00
clerk.opam Upgrade Cmdliner dep 2022-05-09 11:39:18 +02:00
CONTRIBUTING.md more documentation 2022-05-31 14:08:48 +02:00
Dockerfile Add a Dockerfile for builds 2021-09-23 17:08:52 +02:00
dune revert dependency between clerk and catala 2022-06-07 08:54:03 +02:00
dune-project Disable dune generated opam files 2022-05-09 11:34:15 +02:00
flake.lock update lock files 2022-07-11 00:23:12 +00:00
flake.nix calling using self to get the current packages. 2022-05-31 16:59:09 +02:00
french_law.opam Disable dune generated opam files 2022-05-09 11:34:15 +02:00
generate_website_assets.sh Merge branch 'master' into allocations_logement 2022-07-06 16:43:14 +02:00
INSTALL.md Warning about Z3 and the proof platform 2022-03-09 17:03:47 +01:00
LICENSE.txt Code reorg 2019-09-04 10:32:33 +02:00
Makefile Not silent commands 2022-07-13 09:53:20 +02:00
ninja_utils.opam Disable dune generated opam files 2022-05-09 11:34:15 +02:00
README.md docs(clerk): add documentation about clerk and the Ninja_utils module 2022-02-24 14:05:05 +01:00

Catala logo

Catala

Explore the docs »
View TutorialReport BugContributeJoin Zulip Chat

CI Opam Licence Tag LoC Language Issues Contributors Activity

Catala is a domain-specific language for deriving faithful-by-construction algorithms from legislative texts. To learn quickly about the language and its features, you can jump right to the official Catala tutorial. You can join the Catala community on Zulip!


Table of Contents

Concepts

Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.

Concretely, you have to first gather all the laws, executive orders, previous cases, etc. that contain information about the socio-fiscal mechanism that you want to implement. Then, you can proceed to annotate the text article by article, in your favorite text editor :

Screenshot

Once your code is complete and tested, you can use the Catala compiler to produce a lawyer-readable PDF version of your implementation. The Catala language has been specially designed in collaboration with law professionals to ensure that the code can be reviewed and certified correct by the domain experts, which are in this case lawyers and not programmers.

Screenshot

The Catala language is special because its logical structure mimics the logical structure of the law. Indeed, the core concept of "definition-under-conditions" that builds on default logic has been formalized by Professor Sarah Lawsky in her article A Logic for Statutes. The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.

Getting started

To get started, the best place is the tutorial of the language. A French version is also available but might be out of sync with the latest language features.

Building and installation

Catala is available as an opam package! If opam is installed on your machine, simply execute:

opam install catala

To get the cutting-edge, latest version of Catala, you can also do

opam pin add catala --dev-repo

However, if you wish to get the latest developments of the compiler, you probably want to compile it from the sources of this repository or use nix. For that, see the dedicated readme.

Usage

Catala

Use catala --help if you have installed it to get more information about the command line options available. The man page is also available online. To get the development version of the help, run make help_catala after make build. The catala binary corresponds to the Catala compiler.

The top-level Makefile contains a lot of useful targets to run. To display them, use

    make help

Clerk

Use clerk --help if you have installed it to get more information about the command line options available. To get the development version of the help, run make help_clerk after make build. The clerk binary corresponds to the Catala build system, responsible for testing among other things.

To get more information about Clerk, see the dedicated readme

Documentation

Syntax cheat sheet

A complete and handy reference of the Catala syntax can be found in the cheat sheet (for French and English versions of the syntax).

Formal semantics

To audit the formal proof of the partial certification of the Catala compiler, see the dedicated readme.

Compiler documentation

The compiler documentation is auto-generated from its source code using dune and odoc. Use

make doc

to generate the documentation, then open the doc/odoc.html file in any browser. The documentation is also accessible online.

Examples

To explore the different programs written in Catala, see the dedicated readme.

API

To know how to use the code generated by the Catala compiler in your favorite programming language, head to the readme of the French law library

Contributing

To know how you can contribute to the project, see the dedicated readme.

Test suite

To know how to run or improve the Catala reference test suite, see the dedicated readme.

License

The compiler and all the code contained in this repository is released under the Apache license (version 2) unless another license is explicited for a sub-directory.

Limitations and disclaimer

Catala is a research project from Inria, the French National Research Institute for Computer Science. The compiler is yet unstable and lacks some of its features.

Pierre Catala

The language is named after Pierre Catala, a professor of law who pionneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre détudes et de traitement de linformation juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation.