A mathematical formulation of the tax code ?

A mathematical formulation of the tax code?
Reverse engineering the tax code and analysis by automated theorem proving"

I’m going to tell you the story of a mysterious language whose protagonists are the Directorate General of Public Finance (Direction Générale des Finances Publiques or DGFiP) and automatic theorem provers. We will then see how we can use automatic theorem provers to study the tax code and how, more generally, the law can be expressed algorithmically. This story led to the Verifisc project, and paves the way for a reappropriation of the complexity of the French tax system using tools that are accessible to everyone.

▻https://blog.merigoux.fr/en/2019/12/20/taxes-formal-proofs.html
[fr]: Vers une imposition formalisée? Rétro-ingénierie du code des impôts et analyse par preuve automatique ▻https://blog.merigoux.ovh/fr/2019/12/20/impots-formels.html

via ▻https://lobste.rs/s/pfswxd/mathematical_formulation_tax_code