Le code des impôts définit dans son texte législatif une fonction mathématique permettant de calculer l’impôt sur le revenu d’un foyer fiscal. Afin de recouvrer l’impôt, cette fonction est implémentée sous la forme d’un algorithme par la Direction Générale des Finances Publiques (DGFiP), en utilisant un langage dédié appelé M (pour macro-langage). Nous proposons une sémantique formelle du langage M, testée grâce aux données publiées par la DGFiP. Cette formalisation, couplée à la publication par la DGFiP de la base de code M calculant l’impôt, nous donne accès à une formalisation complète de la portion du code des impôts définissant l’algorithme de calcul de l’impôt sur le revenu. Nous démontrons l’utilité d’une telle formalisation grâce à un prototype à base de solveurs SMT permettant d’inférer des méta-propriétés sur le calcul de l’impôt. Ces méta-propriétés peuvent ensuite compléter et affiner les analyses économiques existantes sur les effets redistributifs de l’impôt sur le revenu, mais aussi de diverses allocations. Plus généralement, une formalisation systématique des portions algorithmiques de la loi permettrait d’augmenter le niveau d’assurance sur la cohérence du système socio-fiscal français.
Trois artefacts logiciels accompagnent cet article : une formalisation mécanisée de la sémantique du langage M, un compilateur pour le langage M basé sur cette sémantique, ainsi que le prototype d’encodage du code des impôts dans le solveur SMT Z3.
See also: Gallium’s talk with Denis