mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Update latex so that we can also have doc generated from literate programming tool
Rather than manual text
This commit is contained in:
Denis Merigoux
parent
aa57786e82
commit
2f6d8893f4
@ -28,7 +28,7 @@
|
||||
Nicolas \bsc{Chataing}\\Inria -- École Normale Supérieure\and
|
||||
}
|
||||
|
||||
\newcommand{\cm}[1]{\textbf{\textcolor{Gray}{#1}}}
|
||||
\providecommand{\cm}[1]{\textit{\texttt{\textcolor{PineGreen}{#1}}}}
|
||||
\newcommand{\kw}[1]{\textbf{\textcolor{OliveGreen}{#1}}}
|
||||
\newcommand{\inlinekw}[1]{\kw{\texttt{#1}}}
|
||||
\newenvironment{metadata}{
|
||||
@ -47,71 +47,14 @@
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
\subsection{Quelle garantie pour les calculs de transferts sociaux ?}
|
||||
|
||||
Impôts, allocations et pensions de retraite partagent un point commun : les règles de calcul des montants de ces transferts sociaux sont définies dans des textes législatifs. Ce sont ces textes en langage naturel, votés par le parlement ou décrétés par le gouvernement, qui servent de référence aux administrations et entreprises qui ont besoin de calculer ces montants de transferts. Cependant, ces calculs sont largement effectués automatiquement : il existe donc des programmes informatiques qui suivent les règles définies par la loi pour calculer le montant des transferts sociaux. Dès lors se pose la question suivante : comment être sûr que ces programmes informatiques, écrits dans des langages de programmation, implémentent fidèlement les règles décrites en langage naturel dans les textes législatifs ?
|
||||
|
||||
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. 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 vieux concept d'informatique, la 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. 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.
|
||||
|
||||
\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 pour prévenir toute possibilité de contentieux vis-à-vis du logiciel informatique.
|
||||
|
||||
\paragraph{Cohérence} Ces problèmes de cohérence se posent aussi en droit fiscal et en droit social. Dans ce cas particulier, la cohérence législative repose sur la cohérence mathématique des règles de calcul définies dans les textes. Il s'agit par exemple de 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.
|
||||
\input{motivation.tex}
|
||||
|
||||
\section{Étude de cas : les allocations familiales}
|
||||
Afin de mettre en pratique ces nouveaux concepts, nous vous proposons un exemple d'annotation d'un article de loi définissant les allocations familiales par des morceaux de programmes écrits dans notre nouveau langage de programmation \emph{ad hoc}. Le guide de lecture ci-dessous contient normalement toutes les informations nécessaires à la compréhension des annotations informatiques.
|
||||
|
||||
\subsection{Guide de lecture}
|
||||
|
||||
\paragraph{Objectif} Le but est d’annoter le texte de loi avec un langage informatique correspondant (qu’on appellera « code »). Le langage informatique doit traduire exactement le contenu des articles, sans rien ajouter. Pour une plus grande clarté, le code sera placé dans le texte de loi, aux endroits pertinents. Cela permettra de vérifier localement, ligne à ligne, si le code correspond bien au texte de loi. Ce code sera mis en valeur par une \verb|police différente| et une \textcolor{OliveGreen}{coloration particulière}.
|
||||
|
||||
\paragraph{Avertissement} Ce guide a pour objet de définir les termes utilisés dans le code. Chaque terme défini a été choisi pour permettre une compréhension égale des juristes et informaticiens. Par conséquent, chaque terme a une signification précise en droit et en informatique. La signification retenue ici n’est pas exactement celle du juriste ou de l’informaticien, mais renvoie à des notions que l’un et l’autre comprennent. C’est pourquoi cette étape de définition - ou de syntaxe - doit être lue attentivement.
|
||||
|
||||
\paragraph{Contexte} Le contexte est la description de tous les faits présents dans la réalité que va mentionner le morceau de texte de loi. En informatique, il est nécessaire de définir le contexte applicable à chaque partie du code avec un nom, qui suit le terme \inlinekw{contexte}. Deux morceaux de code peuvent avoir le même contexte s’ils sont désignés par le même terme suivant \inlinekw{contexte}. Ainsi, à chaque fois qu’apparait le terme \inlinekw{contexte}, le code définit son contexte d’application.
|
||||
|
||||
\paragraph{Données} Les données sont les faits présents dans la réalité, dans un contexte donné. Ce sont tous les éléments que le programme va manipuler. Par exemple, dans la proposition suivante « tout enfant jusqu’à la fin de l’obligation scolaire », les données sont (1) l'enfant et (2) la fin de l’obligation scolaire. Ces deux données sont nécessaires et suffisantes pour faire fonctionner le code. Ainsi, chaque fois qu’apparaît le mot donnée, un élément utilisé par la suite dans le code sera déterminé.
|
||||
|
||||
Une donnée, introduite par \inlinekw{donnée}, peut également être annotée par un \inlinekw{contenu}, qui décrit ce que représente cette donnée : un entier pour un nombre d’années, un montant pour un revenu, etc. Cette annotation de contenu est nécessaire en informatique, car c’est ce qui permet d’effectuer les calculs numériques.
|
||||
|
||||
\paragraph{Choix} Parfois, une donnée peut avoir un contenu qui prend plusieurs formes. Par exemple, l’entité en charge d’un enfant est soit un couple soit une personne seule. On exprime cette disjonction de cas en utilisant \inlinekw{choix}, puis en introduisant chacun des cas avec \inlinekw{-}\inlinekw{-}. Lors que l’on veut ensuite utiliser une donnée dont le contenu est un choix, il faut alors examiner chacun des cas avec \inlinekw{selon} $\ldots$ \inlinekw{sous forme}.
|
||||
|
||||
\paragraph{Collections} Autre cas particulier du contenu d’une donnée : si celle-ci fait référence à plusieurs choses. Par exemple, la donnée \texttt{enfants} fait référence à tous les enfants d’un ménage. On exprimera cette multiplicité à l’aide de \inlinekw{collection} et si l’on veut utiliser cette collection de données, on le fera avec \inlinekw{existe} $\ldots$ \inlinekw{dans} $\ldots$ \inlinekw{tel que} et \inlinekw{pour tout} $\ldots$ \inlinekw{dans} $\ldots$ \inlinekw{on a}.
|
||||
|
||||
\begin{metadata}
|
||||
Le contexte et les données correspondent aux métadonnées. Ce sont des éléments qui ne définissent pas de règle juridique précise, mais qui sont nécessaires pour la traduction en langage informatique. C’est pourquoi ces métadonnées sont placées avant les règles et mises en valeur par une boîte colorée, comme ici.
|
||||
\end{metadata}
|
||||
|
||||
|
||||
\paragraph{Champ d’application} Le champ d’application d’un article de loi s’inscrit dans un contexte particulier. Dans le code, il est nécessaire de préciser le champ d’application de chaque article de loi. Ce champ d’application sera introduit par \inlinekw{champ d’application}, suivi d’un nom correspondant à un contexte précédemment défini.
|
||||
|
||||
\paragraph{Règles} Le but du programme est de traduire en langage informatique les règles exprimées dans le texte de loi. Les règles sont donc les éléments du texte législatif qui permettent d’aboutir à des conséquences. Ces conséquences peuvent être : une définition, une règle logique ou ou une assertion. Nous allons définir chacune de ces règles. Cependant, toute règle ne s’applique que si une condition précise est valable. Cette condition est introduite par \inlinekw{sous condition}, et sa conséquence par \inlinekw{conséquence}. Les règles peuvent également manipuler des conditions juridiques introduites par \inlinekw{condition}.
|
||||
|
||||
\paragraph{Règle logique} Une règle permet d’exprimer des relations logiques entre éléments du texte de loi. Elle permet notamment de préciser quand des conditions sont remplies. Les règles logiques sont introduites par le mot \inlinekw{règle}.
|
||||
|
||||
\paragraph{Définition} La définition permet de définir une donnée en fonction d’une autre donnée. Elle permet d’exprimer une donnée en fonction d’une ou plusieurs autres. Elles sont introduites par \inlinekw{définition}.
|
||||
|
||||
\paragraph{Assertions} Les assertions sont, en langage informatique, une condition de cohérence. Le code doit vérifier que les assertions sont toujours vraies lorsqu’il s’exécute. Cela permet d’assurer une cohérence d’ensemble à tout le programme. Les assertions peuvent être très variées et imposer plusieurs types de vérifications. Elles sont exprimées en langage informatique sous le terme \inlinekw{assertion}.
|
||||
\input{reading_guide}
|
||||
|
||||
\subsection{Exemple d'articles de loi annotés}
|
||||
|
||||
@ -309,52 +252,7 @@ NOTA : Décret n° 2008-409 du 28 avril 2008 JORF du 29 avril 2008 art. 2 : Les
|
||||
|
||||
\subsection{Questionnaire de satisfaction}
|
||||
|
||||
Le langage de programmation présenté ci-dessus est toujours à l'étude, et nous souhaitons que le projet bénéficie le plus tôt possible de retours de professionnels susceptibles d'utiliser ou d'être en contact avec ce nouvel outil. Aussi nous vous proposons de nous faire part de vos retours en remplissant le formulaire page suivante. Les questions sont posées dans un ordre croissant de difficulté de compréhension du document. Une fois le formulaire rempli, enregistrez le PDF sous un autre nom et envoyez-le par email aux auteurs aux adresses suivantes:
|
||||
|
||||
\begin{center}
|
||||
\href{mailto:denis.merigoux@inria.fr}{\texttt{denis.merigoux@inria.fr}}\\[0.5em]
|
||||
\href{mailto:huttner.liane@gmail.com}{\texttt{huttner.liane@gmail.com}}\\[0.5em]
|
||||
\href{mailto:nicolas.chataing@ens.fr}{\texttt{nicolas.chataing@ens.fr}}
|
||||
\end{center}
|
||||
|
||||
\clearpage
|
||||
|
||||
\label{form}
|
||||
\begin{Form}
|
||||
\begin{center}
|
||||
\small
|
||||
\textbf{(1) Quel est votre nom et profession ? Vous pouvez également indiquer des détails pertinents sur votre expérience ou parcours.}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(2) Est-ce que vous comprenez la démarche ? Si oui, vous paraît-elle justifiée ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(3) Est-ce que vous arrivez à poser votre regard sur les morceaux de code sans avoir mal à la tête ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(4) Est-ce que vous arrivez à comprendre le sens du code étant donné le guide de lecture au début ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(5) Est-ce que vous arrivez à relier le sens de chacun des morceaux de code au sens du texte législatif qu'il est censé annoté ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(6) Est-ce que vous pouvez certifier que le code fait bien ce que dit la loi et rien de plus ? Si non, est-ce que vous avez trouvé une erreur dans le code ? }\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\end{Form}
|
||||
|
||||
|
||||
\input{questionnaire}
|
||||
|
||||
|
||||
\end{document}
|
||||
|
||||
36
doc/motivation.tex
Normal file
36
doc/motivation.tex
Normal file
@ -0,0 +1,36 @@
|
||||
|
||||
\subsection{Quelle garantie pour les calculs de transferts sociaux ?}
|
||||
|
||||
Impôts, allocations et pensions de retraite partagent un point commun : les règles de calcul des montants de ces transferts sociaux sont définies dans des textes législatifs. Ce sont ces textes en langage naturel, votés par le parlement ou décrétés par le gouvernement, qui servent de référence aux administrations et entreprises qui ont besoin de calculer ces montants de transferts. Cependant, ces calculs sont largement effectués automatiquement : il existe donc des programmes informatiques qui suivent les règles définies par la loi pour calculer le montant des transferts sociaux. Dès lors se pose la question suivante : comment être sûr que ces programmes informatiques, écrits dans des langages de programmation, implémentent fidèlement les règles décrites en langage naturel dans les textes législatifs ? \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. 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 vieux concept d'informatique, la 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. 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.
|
||||
|
||||
\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 pour prévenir toute possibilité de contentieux vis-à-vis du logiciel informatique.
|
||||
|
||||
\paragraph{Cohérence} Ces problèmes de cohérence se posent aussi en droit fiscal et en droit social. Dans ce cas particulier, la cohérence législative repose sur la cohérence mathématique des règles de calcul définies dans les textes. Il s'agit par exemple de 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 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.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.
|
||||
48
doc/questionnaire.tex
Normal file
48
doc/questionnaire.tex
Normal file
@ -0,0 +1,48 @@
|
||||
|
||||
|
||||
Le langage de programmation présenté ci-dessus est toujours à l'étude, et nous souhaitons que le projet bénéficie le plus tôt possible de retours de professionnels susceptibles d'utiliser ou d'être en contact avec ce nouvel outil. Aussi nous vous proposons de nous faire part de vos retours en remplissant le formulaire page suivante.
|
||||
|
||||
Les questions sont posées dans un ordre croissant de difficulté de compréhension du document. N'hésitez pas à faire référence au code dans vos réponses, en citant le numéro de ligne correspondant : chaque ligne de code est en effet annotée d'un numéro sur la gauche.
|
||||
|
||||
Une fois le formulaire rempli, enregistrez le PDF sous un autre nom et envoyez-le par email aux auteurs aux adresses suivantes:
|
||||
|
||||
\begin{center}
|
||||
\href{mailto:denis.merigoux@inria.fr}{\texttt{denis.merigoux@inria.fr}}\\[0.5em]
|
||||
\href{mailto:huttner.liane@gmail.com}{\texttt{huttner.liane@gmail.com}}\\[0.5em]
|
||||
\href{mailto:nicolas.chataing@ens.fr}{\texttt{nicolas.chataing@ens.fr}}
|
||||
\end{center}
|
||||
|
||||
\label{form}
|
||||
\begin{Form}
|
||||
\begin{center}
|
||||
\small
|
||||
\textbf{(1) Quel est votre nom et profession ? Vous pouvez également indiquer des détails pertinents sur votre expérience ou parcours.}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(2) Est-ce que vous comprenez la démarche ? Si oui, vous paraît-elle justifiée ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(3) Est-ce que vous arrivez à poser votre regard sur les morceaux de code sans avoir mal à la tête ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(4) Est-ce que vous arrivez à comprendre le sens du code étant donné le guide de lecture au début ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth, height=12em]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(5) Est-ce que vous arrivez à relier le sens de chacun des morceaux de code au sens du texte législatif qu'il est censé annoté ? Si non, comment améliorer cela ?}\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth, height=12em]{}
|
||||
\end{center}
|
||||
\begin{center}
|
||||
\textbf{(6) Est-ce que vous pouvez certifier que le code fait bien ce que dit la loi et rien de plus ? Si non, est-ce que vous avez trouvé une erreur dans le code ? }\\[1em]
|
||||
|
||||
\TextField[multiline=true, width=\textwidth, height=24em]{}
|
||||
\end{center}
|
||||
\end{Form}
|
||||
27
doc/reading_guide.tex
Normal file
27
doc/reading_guide.tex
Normal file
@ -0,0 +1,27 @@
|
||||
\providecommand{\kw}[1]{\textbf{\textcolor{OliveGreen}{#1}}}
|
||||
\providecommand{\inlinekw}[1]{\kw{\texttt{#1}}}
|
||||
\providecommand{\cm}[1]{\textit{\texttt{\textcolor{PineGreen}{#1}}}}
|
||||
|
||||
\paragraph{Objectif} Le but est d’annoter le texte de loi avec un langage informatique correspondant (qu’on appellera « code »). Le langage informatique doit traduire exactement le contenu des articles, sans rien ajouter. Pour une plus grande clarté, le code sera placé dans le texte de loi, aux endroits pertinents. Cela permettra de vérifier localement, ligne à ligne, si le code correspond bien au texte de loi. Ce code sera mis en valeur par une \inlinekw{police différente et une coloration particulière}.
|
||||
|
||||
\paragraph{Avertissement} Ce guide a pour objet de définir les termes utilisés dans le code. Chaque terme défini a été choisi pour permettre une compréhension égale des juristes et informaticiens. Par conséquent, chaque terme a une signification précise en droit et en informatique. La signification retenue ici n’est pas exactement celle du juriste ou de l’informaticien, mais renvoie à des notions que l’un et l’autre comprennent. C’est pourquoi cette étape de définition -- ou de syntaxe -- doit être lue attentivement.
|
||||
|
||||
\paragraph{Métadonnées} Les métadonnées sont la description de tous les faits présents dans la réalité que va mentionner le morceau de texte de loi. Cette partie du code est nécessaire d'un point de vue informatique afin de donner de la \inlinekw{structure} aux informations manipulées, mais elle est accessoire lorsque l'on veut juste vérifier la cohérence avec le texte de loi.
|
||||
|
||||
Les \inlinekw{données} sont les faits présents dans la réalité, dans un contexte donné. Ce sont tous les éléments que le programme va manipuler. Par exemple, dans la proposition suivante « tout enfant jusqu’à la fin de l’obligation scolaire », les données sont (1) l'enfant et (2) la fin de l’obligation scolaire. Une donnée peut également dépendre d'un paramètre, par exemple un âge limite que dépend \inlinekw{de} l'enfant.
|
||||
|
||||
Une donnée est annotée par un \inlinekw{contenu}, qui décrit ce que représente cette donnée : un entier pour un nombre d’années, un montant pour un revenu, etc. Cette annotation de contenu est nécessaire en informatique, car c’est ce qui permet d’effectuer les calculs numériques. Les \inlinekw{conditions} sont un type particulier de données sans contenu, qui correspondent à des concepts juridiques.
|
||||
|
||||
% Parfois, une donnée peut avoir un contenu qui prend plusieurs formes. Par exemple, l’entité en charge d’un enfant est soit un couple soit une personne seule. On exprime cette disjonction de cas en utilisant \inlinekw{choix}, puis en introduisant chacun des cas avec \inlinekw{-}\inlinekw{-}. Lors que l’on veut ensuite utiliser une donnée dont le contenu est un choix, il faut alors examiner chacun des cas avec \inlinekw{selon} $\ldots$ \inlinekw{sous forme}.
|
||||
|
||||
Autre cas particulier du contenu d’une donnée : si celle-ci fait référence à plusieurs choses. Par exemple, la donnée \texttt{enfants} fait référence à tous les enfants d’un ménage. On exprimera cette multiplicité à l’aide de \inlinekw{collection} et si l’on veut utiliser cette collection de données, on le fera avec \inlinekw{existe} $\ldots$ \inlinekw{dans} $\ldots$ \inlinekw{tel que} et \inlinekw{pour tout} $\ldots$ \inlinekw{dans} $\ldots$ \inlinekw{on a}.
|
||||
|
||||
\paragraph{Champ d’application} Le champ d’application d’un article de loi s’inscrit dans un contexte particulier. Dans le code, il est nécessaire de préciser le champ d’application de chaque article de loi. Ce champ d’application sera introduit par \inlinekw{champ d’application}. Il est également nécéssaire de préciser quelles données seront utilisées dans un champ d'application ; cela est fait à la fin de la section métadonnées.
|
||||
|
||||
Le texte de loi sera donc saucissonné par des blocs de code, tous introduits par leur champ d'application. À l'intérieur du code, des messages n'ayant pas valeur informatique mais laissés à titre de commentaires seront introduits par \cm{\#} et \cm{écrits dans cette police}.
|
||||
|
||||
\paragraph{Règles} Le but du programme est de traduire en langage informatique les règles exprimées dans le texte de loi. Les règles sont donc les éléments du texte législatif qui permettent d’aboutir à des conséquences. Toute règle ne s’applique que si une condition précise est valable. Cette condition est introduite par \inlinekw{sous condition}, et sa conséquence par \inlinekw{conséquence}.
|
||||
|
||||
Basiquement, une \inlinekw{règle} permet d’exprimer des relations logiques entre concepts du texte de loi. Elle permet notamment de préciser quand des \inlinekw{conditions} sont remplies. La \inlinekw{définition} permet de définir une donnée présente dans le champ d'application en fonction d’une autre donnée, par exemple pour exprimer une règle de calcul.
|
||||
|
||||
Les \inlinekw{assertions} sont, en langage informatique, une condition de cohérence. Le code doit vérifier que les assertions sont toujours vraies lorsqu’il s’exécute. Cela permet d’assurer une cohérence d’ensemble à tout le programme. Les assertions peuvent être très variées et imposer plusieurs types de vérifications.
|
||||
@ -98,7 +98,7 @@
|
||||
}
|
||||
}
|
||||
{
|
||||
'match' : '\\b(existe|selon|sous\\s+forme|fixé\\s+par|décroissante|croissante|varie\\s+avec|on\\s+a|tel\\s+que|pour\\s+tout|nombre)\\b'
|
||||
'match' : '\\b(existe|selon|sous\\s+forme|fixé\\s+par|décroissante|croissante|varie\\s+avec|on\\s+a|dans|tel\\s+que|pour\\s+tout|nombre)\\b'
|
||||
'name' : 'keyword.control.lawspec'
|
||||
}
|
||||
{
|
||||
|
||||
@ -190,7 +190,7 @@ code : context {
|
||||
}
|
||||
|
||||
: pattern {
|
||||
regex \= \b(existe|selon|sous\s+forme|fixé\s+par|décroissante|croissante|varie\s+avec|on\s+a|tel\s+que|pour\s+tout|nombre)\b
|
||||
regex \= \b(existe|selon|sous\s+forme|fixé\s+par|décroissante|croissante|varie\s+avec|on\s+a|dans|tel\s+que|pour\s+tout|nombre)\b
|
||||
styles [] = .keyword_expression ;
|
||||
}
|
||||
|
||||
|
||||
@ -36,7 +36,7 @@ class LawspecLexer(RegexLexer):
|
||||
# (u'(\\*\\/)', bygroups(Generic.Prompt), '#pop'),
|
||||
(u'(\\s*\\#.*$)', bygroups(Comment.Single)),
|
||||
(u'(donn\xe9e|condition|contexte)(\\s+)([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)', bygroups(Keyword.Declaration, Text, Name.Variable)),
|
||||
(u'\\b(existe|selon|sous\\s+forme|fix\xe9\\s+par|d\xe9croissante|croissante|varie\\s+avec|on\\s+a|tel\\s+que|pour\\s+tout|nombre)\\b', bygroups(Keyword)),
|
||||
(u'\\b(existe|selon|sous\\s+forme|fix\xe9\\s+par|d\xe9croissante|croissante|varie\\s+avec|on\\s+a|dans|tel\\s+que|pour\\s+tout|nombre)\\b', bygroups(Keyword)),
|
||||
(u'\\b(champ\\s+d\'application|si\\s+et\\s+seulement\\s+si|d\xe9pend|de|d\xe9claration|inclus|collection|contenu|optionnel|structure|contexte|r\xe8gle|sous condition|cons\xe9quence|rempli|\xe9gal\\s+\xe0|assertion|d\xe9finition)\\b', bygroups(Keyword.Declaration)),
|
||||
(u'\\b(vrai|faux|[0-9]+(\\.[0.9]*|))\\b', bygroups(Keyword.Constant)),
|
||||
(u'\\b([0-9]+(\\.[0.9]*|))\\b', bygroups(Number)),
|
||||
|
||||
@ -6,6 +6,8 @@
|
||||
\usepackage{lmodern}
|
||||
\usepackage{minted}
|
||||
\usepackage{textcomp}
|
||||
\usepackage[hidelinks]{hyperref}
|
||||
\usepackage[dvipsnames]{xcolor}
|
||||
\usepackage{fullpage}
|
||||
|
||||
\fvset{
|
||||
@ -17,7 +19,11 @@
|
||||
codes={\catcode`\$=3\catcode`\^=7}
|
||||
}
|
||||
|
||||
\title{Implémentation du calcul des allocations familiales}
|
||||
\title{
|
||||
Proposition d'un langage de formalisation\\
|
||||
de textes législatifs :\\
|
||||
Questionnaire à l'intention de juristes
|
||||
}
|
||||
\author{
|
||||
Denis \bsc{Merigoux}\\Inria\and
|
||||
Liane \bsc{Huttner}\\Université Panthéon-Sorbonne\and
|
||||
@ -29,8 +35,19 @@
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
\section{Implémentation}
|
||||
\input{../doc/motivation}
|
||||
|
||||
\section{Implémentation des allocations familiales}
|
||||
Afin de mettre en pratique ces nouveaux concepts, nous vous proposons un exemple d'annotation d'un article de loi définissant les allocations familiales par des morceaux de programmes écrits dans notre nouveau langage de programmation \emph{ad hoc}. Le guide de lecture ci-dessous contient normalement toutes les informations nécessaires à la compréhension des annotations informatiques.
|
||||
|
||||
\subsection{Guide de lecture}
|
||||
|
||||
\input{../doc/reading_guide}
|
||||
|
||||
\input{allocations_familiales_new}
|
||||
|
||||
\section{Questionnaire de satisfaction}
|
||||
|
||||
\input{../doc/questionnaire}
|
||||
|
||||
\end{document}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user