Update after Alice's feedback

doc/motivation.tex

@@ -1,7 +1,5 @@
-
 \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
@@ -10,23 +8,28 @@ Impôts, allocations et pensions de retraite partagent un point commun : les rè
 
 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 ?
+%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 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.
+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. 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.
+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 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 pour prévenir toute possibilité de contentieux vis-à-vis du logiciel informatique.
+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} 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.
+\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.
 

doc/questionnaire.tex

@@ -12,6 +12,7 @@ Une fois le formulaire rempli, enregistrez le PDF sous un autre nom et envoyez-l
   \href{mailto:nicolas.chataing@ens.fr}{\texttt{nicolas.chataing@ens.fr}}
 \end{center}
 
+\clearpage
 \label{form}
 \begin{Form}
   \begin{center}
@@ -43,6 +44,6 @@ Une fois le formulaire rempli, enregistrez le PDF sous un autre nom et envoyez-l
   \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]{}
+    \TextField[multiline=true, width=\textwidth, height=28em]{}
   \end{center}
 \end{Form}

test/wrapper.tex

@@ -33,6 +33,11 @@
 \begin{document}
 \maketitle
 \renewcommand{\contentsname}{Sommaire}
+
+\begin{abstract}
+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 ? Après avoir résumé l'état de l'art en la matière, nous proposons et décrivons un processus nouveau permettant d'atteindre une garantie de conformité bien supérieure. Nous illustrons ensuite la manière dont ce processus fonctionne sur l'exemple des allocations familiales. En fin de document, un questionnaire vous permet de nous transmettre vos remarques sur notre démarche et sur le processus.
+\end{abstract}
+
 \tableofcontents
 
 \section{Introduction}