A Modern Compiler for the French Tax Code

mix... A slide of the story: https://www.slideshare.net/Etalab/opening-up-the-french-tax-... But I believe it should be mandatory for the state to provide the source of every softwares they use internally to manage our lives. Also a test suite to allow any citizen to validate their own effort to comply with the law. Just like laws should be published as diff of the previous laws, in a VCS repo.

[18, 19], pointing out the legal ambiguities in the text of the law that need to be resolved using legal reasoning. She also claims that the tax law drafting style follows default logic [24], a non-monotonic logic that is hard to encode in languages with first-order logic (FOL). This could explain, as M is also based on FOL, the complexity of the DGFiP codebase. See https://en.wikipedia.org/wiki/Default_logic and https://en.wikipedia.org/wiki/Non-monotonic_logic But note that it's written in that "style", not that it's done consistently or correctly. Unfortunately I couldn't easily find a copy of the cited papers, but I made a note for later reference. EDIT: I once took a class in law school taught by a Professor of Systems Engineering from the parent university. I forget why, but long ago he took an interest in the rules of evidence in the common law. While the rules evolved organically over more than a thousand years, they actually strongly reflect a formal system of abductive reasoning: https://en.wikipedia.org/wiki/Abductive_reasoning. And there's significant, hidden rigor. In one project he had everyone in class create a tree consisting of evidence (e.g. size 7 shoe) at the leaves, with the branches as inferences all the way up to the top, which was the core legal claim--1) Jim did 2) break and 3) enter into 4) said building.... Anyhow, being a programmer I decided to create my tree using the DOT language and render it using Graphviz. While I was doing that it occurred to me that some of the more esoteric, technical rules of evidence, such as that any piece of evidence can only be used to prove a single element, actually ensures that the tree is an acyclic graph. I'm not sure precisely why (perhaps the professor had more insight), but I believe it's because the rules are in part crafted to ensure that the finder of fact is presented with a tractable problem to solve. The process would get too confusing (and possibly logically inconsistent?) if you didn't keep the tree of evidence and inference simple. No judge or lawmaker likely ever had in mind the literal shape of the evidence tree. In fact, AFAIU nobody thought to represent it as a tree until the late 19th century, when the famous scholar of common law evidence, John Wigmore (https://en.wikipedia.org/wiki/John_Henry_Wigmore), developed a system for analyzing and preparing trial evidence in that manner. Anyhow, a proper and infinitely more rigorous treatment of this is presented in the book, "Analysis of Evidence, 2nd Ed." by Terence Anderson, David Schum, and William Twining. (Schum taught the class.) A large part of the book explores and explains the law of evidence as a system of Bayesian reasoning. (Oh, that's why! I think Prof. Schum first stumbled into the legal realm after he got the idea of using Bayesian statistics to resolve historically famous and contentious legal trials.)