catala/doc/motivation.tex

\subsection{Quelle garantie pour les calculs de transferts sociaux ?}

% \href{https://github.com/betagouv/mon-entreprise/issues/796#issuecomment-608446936}{Des mots mêmes d'un développeur} du simulateur \href{https://mon-entreprise.fr}{\texttt{mon-entreprise.fr}} pour le calcul des cotisation sociales, cette fidélité est loin d'être acquise:
%
% \begin{quote}\itshape
%   Il faut garder en tête que les implémentations des règles socio-fiscales qui existent aujourd'hui (logiciels de paie, simulateurs des conseillers en gestion de patrimoine, outils des URSSAF, etc.) sont loin d'avoir un niveau d'assurance optimal, ou pour le dire plus clairement il y a des erreurs partout. Pour prendre un sujet d'actualité, je ne suis pas sûr qu'il existe beaucoup d'implémentations correctes des indemnités de chômage partiel par exemple (alors que ça concerne au moins 4 millions de salariés). Il a un décalage entre les textes de lois et leur application, et ça représente parfois des différences de quelques centaines de millions d'euros en agrégé (retraite des auto-entrepreneurs ou des artistes-auteurs par exemple). Bref, tout ça pour dire que si l'on vise bien le meilleur niveau de fiabilité possible, il ne faut pas idéaliser le système tel qu'il fonctionne aujourd'hui.
% \end{quote}

Il existe plusieurs manières d'obtenir des garanties de fidélité des programmes par rapport aux textes. La manière la plus simple, actuellement utilisée par la plupart des administrations et entreprises, consiste à faire rédiger par des juristes des études de cas où le calcul est détaillé pour une situation individuelle. Les programmeurs informatiques peuvent ainsi vérifier que le détail et le résultat du calcul informatique sur cette situation correspondent bien à ce qu'ont écrit les juristes. La garantie apportée par ces études de cas est proportionnelle à leur nombre et à leur diversité : si une règle de calcul n'est pas couverte par une de ces études de cas, elle ne sera pas couverte pas la garantie.

%De manière plus subtile, il ne suffit pas de couvrir toutes les règles de calcul par des études de cas pour obtenir une garantie complète de fidélité. En effet, le comportement de la règle de calcul dépend des valeurs des montants en présence. Pour obtenir une garantie complète de complexité, il faudrait ainsi couvrir par des études de cas tous les comportements possibles de toutes les règles de calcul en présence.
Mais même en couvrant toutes les règles par des études de cas, on n'a toujours pas la garantie que le code soit testé dans tous ses comportements possibles. Le nombre d'études nécessaire pour atteindre cet objectif, difficile à quantifier, est très élevé et en pratique jamais atteint. Dès lors, comment faire pour obtenir la garantie complète de fidélité du programme informatique par rapport à la loi ?

Plutôt que d'évaluer le programme informatique par l'extérieur avec des études de cas, nous proposons une approche alternative basée sur un concept éprouvé en informatique, la \textbf{programmation littéraire}. Le principe de la programmation littéraire est de mêler dans une même source le code informatique ainsi que la description en langage naturel de ce que le code est censé faire. Dans notre cas, cette description en langage naturel est également la source de vérité sur le comportement du programme informatique : les textes législatifs.

Concrètement, cela consiste à partir du texte législatif et annoter ligne à ligne le texte juridique par une traduction informatique fidèle qui retranscrirait tout le contenu sémantique de la ligne de texte, et rien que ce contenu. En procédant ainsi, le problème de la garantie globale de fidélité du programme informatique par rapport à la loi est réduit à la vérification locale de la fidélité d'un morceau de code par rapport à une ligne du texte législatif. Cette vérification demande une grande expertise juridique, car il s'agit de connaître précisément l'interprétation du texte législatif dans toutes les situations possibles.

Notre objectif est de rendre possible cette vérification par des juristes spécialisés. Nous devons pour cela nous donner un langage de programmation qui permette à la fois d'annoter le texte de loi par son équivalent informatique, mais également être compréhensible par des juristes moyennant une formation minimale. Or, la structure logique des textes loi est incompatible avec la structure logique des langages de programmation traditionnels ; il nous faut donc en créer un nouveau.
%Il faut donc que les annotations sous forme de code soient compréhensibles par ces juristes moyennant une formation minimale. Pour cela, il est nécessaire de créer un nouveau langage de programmation qui répond à cette contrainte de lisibilité.

L'annotation des textes législatifs par des programmes rédigés dans ce nouveau langage de programmation correspond au concept de formalisation : il s'agit de donner une définition précise au sens mathématique à toutes les règles de calcul décrites dans la législation.

\subsection{Pour une législation socio-fiscale formalisée}

% Nous affirmons que la méthode basée sur la programmation littéraire des textes législatifs que nous proposons apporterait un progrès significatif par rapport aux méthodes actuelles de production des implémentations informatiques de ces textes, c'est à dire du code qui calcule ce que décrit la loi. Ce progrès se décline en trois principaux axes.
Nous proposons une méthode basée sur la programmation littéraire des textes législatifs. Cette méthode apporterait un progrès significatif par rapport aux méthodes actuelles de production des implémentations informatiques de ces textes (c'est-à-dire de production du code qui calcule ce que décrit la loi). Nous présentons ici les trois principaux avantages qu'apporteraient ce progrès : la sécurité juridique, la cohérence, et enfin la transparence.

\paragraph{Sécurité juridique} Contrairement au langage naturel, un langage de programmation ne laisse pas de place à l'imprécision et à l'incohérence. Lors de l'implémentation d'un programme censé suivre des textes de loi, le programmeur est obligé de faire des décisions arbitraires. Par exemple, si la loi spécifie une règle différente selon que le montant des revenus soit en dessous ou au-dessus d'un certain seuil, le programmeur doit décider arbitrairement ce qui se passe quand le montant des revenus est égal au seuil. La revue du code par un juriste spécialisé permettrait de vérifier que ces choix arbitraires sont des interprétations valides du texte législatif.

Plus globalement, la garantie d'une implémentation en code informatique fidèle au texte législatif apporte un très haut niveau de sécurité juridique à l'organisation qui utiliserait cette technique. Le champ des méthodes formelles, sur lequel repose la théorie derrière cette proposition, est utilisé dans tous les secteurs d'activité critiques tels que le transport (aérien et ferroviaire), la cryptographie, le domaine spatial et même le contrôle des centrales nucléaires. Un contentieux soulevé par une mauvaise implémentation d'un texte législatif peut avoir de lourdes conséquences si cette implémentation est utilisée à grande échelle. Dans ce cas, les processus utilisés en méthodes formelles sont tout à fait adaptés et permettraient de prévenir toute possibilité de contentieux vis-à-vis de la conformité du logiciel informatique.

\paragraph{Cohérence} La cohérence législative, dont le Conseil d'État est le gardien, est également un enjeu en droit fiscal et en droit social. Il s'agit entre autres de vérifier que les décrets et règlements sont conformes aux articles de loi dont ils précisent les conditions d'application. Dans le cas particulier des transferts sociaux, la cohérence législative repose sur la cohérence mathématique des règles de calcul définies dans les textes. Par exemple, il faut vérifier que le montant d'une allocation est bien dégressif par rapport aux revenus du ménage, ou bien que le taux marginal d'imposition ne peut dépasser un certain seuil. La formalisation des règles de calcul permet d'étudier ces règles en tant qu'objets mathématiques, et ainsi de prouver comme théorème la cohérence législative.

Un deuxième aspect de la cohérence législative concerne l'existence même de plusieurs versions du code informatique traduisant un même texte législatif. Si plusieurs organisations possèdent chacune leur programme informatique censé respecter le même texte législatif, comment s'assurer que ces implémentations sont bien cohérentes ? D'un point de vue économique, l'existence même de plusieurs implémentations concurrentes d'un même texte législatif est contre-productive en termes de maintenance. Pour cette raison, l’implémentation à base de programmation littéraire que nous proposons servirait d’implémentation unique de référence du texte législatif, partagée par toutes les organisations qui en auraient besoin. De cette manière, la cohérence de l’interprétation de la loi par l’implémentation informatique serait garantie.

\paragraph{Transparence} La nécessité d'une implémentation unique de référence pour les textes législatifs nous amène naturellement à l'enjeu de la transparence. En effet, pour qu'elle puisse bénéficier à l'ensemble des organisations qui en auraient besoin, l'implémentation de référence doit être publiée en open-source. L'ouverture du code source de ces implémentations considérées comme documents administratifs est une obligation légale depuis la loi 2016-1321 du 7 octobre 2016 pour une République numérique, confirmée par la décision du tribunal administratif de Paris du 18 février 2016 en ce qui concerne l'implémentation du calcul de l'impôt sur le revenu.

L'ouverture du code source possède également l'avantage de permettre un processus collaboratif d'écriture et de validation de l'implémentation entre les diverses organisations concernées. Concrètement, si l'implémentation est publiée par une administration publique, elle pourrait recueillir avant mise en production d'éventuels commentaires ou questions d'organisations privées ou associatives afin de préciser et d'affiner certains choix d'interprétation \emph{ex ante}, évitant ainsi de recourir au contentieux \emph{ex post}.

Pour ces raisons, l'utilisation de notre méthode à base de programmation littéraire nous apparaît comme plus avantageuse à tout point de vue que les méthodes actuelles de validation par études de cas. Les programmes écrits dans le nouveau langage de programmation seront ensuite traduits (« compilés ») vers d'autres langages de programmation plus traditionnels pour être exécutés au sein d'applications informatiques.