Chaque année, près de 37 millions de foyers fiscaux sont concernés par l’impôt sur le revenu. Celui-ci, calculé à partir des déclarations individuelles des contribuables et des informations dont l’administration dispose, tient compte de tous les éléments concernant leurs revenus et charges ainsi que leur situation, permettant ainsi d'avoir un prélèvement au plus juste par rapport à la situation de chacun et d'éviter toute régularisation ultérieure.
La "calculette" de la DGFiP : entre robustesse et rapidité
L'architecture logicielle effectuant ce calcul (appelée "calculette") s’appuie sur un langage dédié, le langage M, développé dans les années quatre-vingt-dix par le bureau SI-1E de la Direction générale des Finances publiques (DGFiP).
Considérée comme extrêmement performante, cette calculette permet à l'heure actuelle de traiter l'intégralité du calcul de l'impôt sur le revenu pour tous les foyers fiscaux en moins de 16 heures (soit environ 650 foyers fiscaux par seconde). Celle-ci peut également se targuer de s’être continuellement adaptée, ces trente dernières années, aux exigences législatives croissantes. Ces dernières nécessitent en effet une mise à jour annuelle de la base de code suivant les modifications du barème de l'impôt sur le revenu, votées en loi de finances.
Une solution qui atteint ses limites
Malgré cela, le paysage informatique a profondément évolué depuis les années quatre-vingt-dix : les compétences sur les technologies employées sur la calculette se raréfient. De même, le paysage de la législation fiscale a beaucoup évolué ; pour s’y adapter, des contournements ont dû être employés pour dépasser certaines limites du langage M.
Les méthodes formelles sont un domaine de l'informatique centré sur l'analyse mathématique des logiciels et des langages de programmation, dans le but d'accroître leur sûreté, leur efficacité ou leur sécurité. Inria est considéré comme un acteur de pointe dans ce domaine, au niveau mondial. L’institut est notamment reconnu pour son assistant d'aide à la preuve Coq.
La solution : réviser cette infrastructure avec des technologies récentes, afin de proposer un nouveau compilateur en mesure de supporter les mises à jour, mais également d’ouvrir de nouveaux champs d'application tels que l'interopérabilité de la calculette avec de nouveaux outils. C’est ce qu’ont fait deux chercheurs en informatique, spécialistes du domaine des méthodes formelles : Denis Merigoux (Prosecco – Inria Paris) et Raphaël Monat (APR - LIP6 - CNRS - Sorbonne Université). « Ma spécialité de recherche, c’est de considérer les programmes comme des objets mathématiques sur lesquels on peut travailler pour améliorer leurs résultats. Et c’est ce que j’ai fait avec le code des impôts », explique Denis Merigoux.
Denis Merigoux et Raphaël Monat ont pu accéder au code source de la "calculette" dans le cadre d’un accord de confidentialité sur les parties critiques de ce code signé avec la DGFiP. Avec l’appui des experts du bureau SI-1E, ils ont exploré en profondeur le langage M et son compilateur puis ont proposé une rénovation, basée sur les techniques de l'état de l'art scientifique.
Mlang, un compilateur moderne pour le calcul de l’impôt sur le revenu
Cette rénovation a débouché sur l'écriture d'un nouveau compilateur, appelé Mlang, créé en utilisant le langage Ocaml (développé par Inria) et publié sous licence libre. Un article de recherche détaillant le fonctionnement de Mlang a également été écrit avec l’aide de Jonathan Protzenko (Microsoft Research, membre du Microsoft Research-Inria Joint Center).
Testé et approuvé par la DGFiP, Mlang fait désormais l'objet d'un transfert de technologie vers le bureau SI-1E, qui a décidé de prolonger ces travaux pour remplacer le compilateur originel de M. Ce remplacement, dont les travaux débuteront en mars prochain, devrait être effectif dans un à deux ans. Il permettra ainsi de fiabiliser sur le long terme les caractéristiques et la sémantique du langage, mais aussi d’ajouter de nouvelles fonctionnalités au langage M au travers de l'utilisation de techniques modernes de compilation. À terme, le code des impôts pourra ainsi s'accompagner d'une preuve de correction.
Un travail main dans la main entre recherche publique et administration
Un travail qui n’aurait pas été réalisable sans la mise en "open source" du code de l'algorithme de calcul de l'impôt sur le revenu. Publié depuis 2016 par l’entremise d’Etalab, celui-ci a servi de point de départ aux investigations des chercheurs.
Dans cet esprit, Mlang est, lui aussi, distribué sous licence libre. Il permet de répliquer exactement le calcul primitif de l'impôt, tel qu'il figure sur l’avis d'imposition des citoyens. De quoi améliorer leur confiance dans le calcul de l'impôt sur le revenu, en leur donnant la possibilité d’accéder à l’algorithme, et d’en comprendre le résultat.