More more doc

README.md

@@ -1,9 +1,86 @@
 # Catala
 
-Catala is a domain-specific language for deriving faithful-by-construction algorithms
-from legislative texts.
+Catala is a domain-specific language for deriving
+faithful-by-construction algorithms from legislative texts.
 
-## OCaml requirements
+## 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 :
+
+<center>
+![Image of Yaktocat](doc/ScreenShotAtom.png)
+</center>
+
+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.
+
+<center>
+![Image of Yaktocat](doc/CatalaScreenShot.png)
+</center>
+
+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 of Law Sarah Lawsky in her article [A Logic for Statutes](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3088206). 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.
+
+
+## Catala motivating example : French "allocations familiales"
+
+In the `example/allocations_familiales` folder, you will find the
+`allocations_familiales.catala` file which contains the
+algorithm computing French family benefits. The algorithm consists of annotations to the legislative
+texts that define the family benetifs, using the literate programming paradigm. The Catala
+compiler can extract from the `.catala` file a lawyer-readable version of the annotated text.
+
+Currently, this lawyer-readable version comes in the form of a LaTeX document.
+You will need to have a standard LaTeX distribution installed as well as the
+`latexmk` build tool in order to enjoy the automated document generation process.
+
+To get that lawyer-readable version (which is a LaTeX-created) PDF, simply use
+
+    make allocations_familiales
+
+from the repository root, once you have managed to install the
+compiler (see bewlow). You can then open `examples/allocations_familiales/allocations_familiales.pdf`
+
+## Limitations and disclaimer
+
+### Early stage project
+
+Catala is a research project from Inria, the French National
+Research Institute for Computer Science. The compiler is yet very
+unstable and lacks most of its features. Currently, it only
+parses the surface language to producde the lawyer-readable PDF,
+no interpreter or compiler backend is provided.
+
+However, the language is bound to have a complete formal semantics
+in the near future. This semantics will guide the compiler
+implementation.
+
+### Languages
+
+Currently, the Catala language only enjoys a French surface
+language, adapted to French law. However, it is perfectly
+possible to craft new parsers for new surface languages adapted
+to English, Spanish, etc. Contact the authors if you are interested.
+
+## The Catala compiler
+
+### OCaml requirements
 
 The Catala compiler is written using OCaml. To install OCaml on your machine and
 if you're running Linux ou MacOS, open a terminal and enter :
@@ -17,7 +94,6 @@ Next, install all the build dependencies with
 
 This should ensure everything is set up for developping on Catala !
 
-## The Catala compiler
 
 ### Installation
 
@@ -71,24 +147,16 @@ support. You can use this virtual environnement with
 The `pigmentize` executable, used for instance by the `minted` LaTeX package,
 will now point to the Catala-enabled version inside the virtual environment.
 
-## Catala motivating example : French "allocations familiales"
+## Contributing
 
-In the `example/allocations_familiales` folder, you will find the
-`allocations_familiales.catala` file which contains the
-algorithm computing French family benefits. The algorithm consists of annotations to the legislative
-texts that define the family benetifs, using the literate programming paradigm. The `catala`
-compiler can extract from the `.catala` file a lawyer-readable version of the annotated text.
+The project accepts pull requests. Please email the authors
+if you are interested, whether you are a law professional, a
+computer scientist or a developer. Please use this email address :
 
-Currently, this lawyer-readable version comes in the form of a LaTeX document.
-You will need to have a standard LaTeX distribution installed as well as the
-`latexmk` build tool in order to enjoy the automated document generation process.
-
-To get that lawyer-readable version (which is a LaTeX-created) PDF, simply use
-
-    make allocations_familiales
-
-from the repository root. You can then open `examples/allocations_familiales/allocations_familiales.pdf`
+    denis DOT merigoux AT inria DOT fr
 
+Please note that the copyright of this code is owned by Inria;
+by contributing, you disclaim all copyright interests in favor of Inria.
 
 ## License