The thesis is available here.
The thesis is divided into two parts, the first dealing with formal verification and programming language design in the abstract. The second part applies that theory to two test cases, one of which is Legal Expert Systems. This part of the thesis has a chapter describing the M++ language that was developed by reverse-engineering the government of France’s tax authority’s systems, and a chapter describing the design and implementation of Catala.
The Catala chapter, in particular, is very interesting for Rules as Code practitioners. It starts with an evaluation of the complex semantic structures used inside statutory law, and then describes how Catala is designed to facilitate literate encodings of that legislation.
It also contains some preliminary evidence on the readability of Catala for legal subject matter experts, and on the time and personnel costs associated with large digitization projects implemented in Catala. Denis anticipates the entire US tax code could be encoded by a small team in 2 years.
It is a very good read, in particular to help understand the need for domain-specific tools in computational law.