Résumé technique : Développement piloté par les protocoles (PDD)

Énoncé du problème

L'essor de la synthèse automatisée de programmes a considérablement réduit le coût marginal de production des implémentations logicielles candidates. Cependant, ce changement crée un goulot d'étranglement critique en matière de gouvernance : déterminer quels artefacts générés sont admissibles au sein d'un système logiciel. Les approches traditionnelles souffrent de limitations spécifiques dans ce contexte :

• Développement piloté par les spécifications (SDD) : Les spécifications en langage naturel sont sémantiquement ambiguës, entraînant une dérive d'interprétation et des hypothèses incohérentes entre différents ingénieurs ou systèmes génératifs.
• Développement piloté par les tests (TDD) : Bien que les tests fournissent des preuves exécutables, ils sont extensionnels (vérifiant des cas sélectionnés) plutôt qu'intensionnels (définissant l'espace complet des implémentations admissibles). Ils échouent souvent à capturer les contrats structurels, les limites d'autorité ou les contraintes opérationnelles telles que les limites de latence et les restrictions d'effets de bord.
• La « taxe du langage naturel » : Le coût récurrent de l'interprétation, de la réconciliation et de la maintenance de descriptions textuelles ambiguës crée un fossé entre l'intention et les contraintes applicables.

Lorsque le code peut être synthétisé et régénéré à faible coût, le code source devient moins durable que les contraintes déterminant son admissibilité. Le défi central se déplace de « comment implémenter » vers « quelles contraintes chaque implémentation acceptable doit satisfaire ».

Méthodologie : Développement piloté par les protocoles (PDD)

Le PDD propose un modèle de développement où l'artefact logiciel principal est un protocole exécutable par machine plutôt que du code d'implémentation. Ce modèle traite les implémentations comme des réalisations remplaçables découvertes par une recherche contrainte, admises uniquement si elles satisfont le protocole gouvernant et produisent des preuves vérifiables.

Le formalisme du protocole

Un protocole $P$ est défini comme un triplet $P = (S, B, O)$, où la conjonction de ces trois classes invariantes définit l'espace d'implémentation admissible ($I_P$) :

1. Invariants structurels ($S$) : Contraintes rigides de type et de schéma sur les entrées, les sorties, les signatures d'interface et les règles de versionnage (par exemple, JSON Schema, OpenAPI, Protocol Buffers). Ceux-ci assurent une poignée de main typée.
2. Invariants comportementaux ($B$) : Prédicats sémantiques qui doivent être vrais pour toutes les entrées et tous les états valides (par exemple, idempotence, déterminisme, monotonie). Ceux-ci sont encodés sous forme d'assertions basées sur les propriétés ou de lois logiques plutôt que de cas de test spécifiques.
3. Invariants opérationnels ($O$) : Limites de capacités explicites couvrant les effets de bord, les dépendances externes, la latence, la consommation de mémoire et les quotas de ressources. Ceux-ci fonctionnent comme des manifestes de capacités ou des limites de politique.

La boucle de validation

Le PDD introduit un modèle architectural séparant le cycle de vie du logiciel en rôles distincts :

1. Rédaction du protocole : Traduction de l'intention architecturale en un triplet exécutable par machine $(S, B, O)$.
2. Génération d'implémentation : Des générateurs automatisés parcourent l'espace d'implémentation pour trouver des candidats satisfaisant le protocole.
3. Validation : Un moteur de validation effectue trois couches de vérifications :
   • Validation structurelle (conformité de l'interface).
   • Validation comportementale (tests basés sur les propriétés, relations métamorphiques).
   • Validation opérationnelle (exécution en bac à sable pour vérifier les limites de capacités).
4. Acceptation productrice de preuves : Une implémentation n'est admise que si le validateur émet une chaîne de preuves signée. Cette chaîne lie cryptographiquement la version du protocole, l'artefact d'implémentation, l'identité du validateur et les résultats de la validation.

Fondements théoriques

L'article formalise le PDD à travers plusieurs relations clés :

• Ensemble d'implémentations admissibles : $I_P = I_S \cap I_B \cap I_O$. Le protocole définit une région de l'espace d'implémentation, et non un programme unique.
• Substituabilité au niveau du protocole : Deux implémentations sont substituables si elles satisfont toutes deux $P$ et que le client ne dépend que des garanties impliquées par $P$. Cela permet la régénération et l'optimisation sans rompre les dépendances en aval, à condition que ces dépendances soient « respectueuses du protocole ».
• Correction : Un validateur est correct s'il n'admet que des implémentations satisfaisant le protocole. L'article postule que l'admission n'a de sens que par rapport à un validateur correct et à un protocole spécifié.

Contributions clés

L'article apporte les contributions spécifiques suivantes :

1. Proposition de cadre : Introduit le PDD comme un cadre traitant les protocoles, et non le code, comme l'artefact durable de l'ingénierie automatisée.
2. Formalisation : Définit un protocole comme un triplet d'invariants structurels, comportementaux et opérationnels définissant conjointement un espace d'implémentation admissible.
3. Relations fondamentales : Définit la conformité au protocole, la substituabilité au niveau du protocole et l'acceptation productrice de preuves comme les relations gouvernant l'admission.
4. Modèle architectural : Décrit la boucle de validation, séparant la rédaction du protocole, la génération, la validation et la préservation des preuves.
5. Nouveaux artefacts : Introduit les chaînes de preuves et les journaux de découverte pour lier les candidats aux résultats de validation et à la provenance, permettant l'auditabilité et la rejouabilité.
6. Analyse conceptuelle : Caractérise la « taxe du langage naturel » et soutient que les protocoles exécutables par machine offrent une voie disciplinée de l'intention narrative vers des conditions d'admissibilité explicites.
7. Synthèse : Relie le PDD aux méthodes formelles, aux tests basés sur les propriétés, à la politique en tant que code, à la provenance logicielle et à la gouvernance d'exécution pour les systèmes autonomes.

Résultats et affirmations

L'article ne présente pas de résultats expérimentaux empiriques (par exemple, performances de référence ou métriques d'étude de cas) mais propose plutôt une proposition théorique et architecturale. Ses affirmations sont formulées comme des hypothèses pour une validation empirique future :

• Changement de gouvernance : Le PDD déplace l'aspect « durable » de l'ingénierie logicielle du code transitoire vers le protocole et la preuve de conformité.
• Réduction de l'ambiguïté : En remplaçant les énoncés descriptifs par des assertions restrictives, le PDD vise à réduire la divergence structurelle, comportementale et opérationnelle (la « taxe du langage naturel »).
• Régénération sûre : Le modèle prétend permettre la régénération sûre d'implémentations (par exemple, migration de langage, optimisation) tant que la nouvelle implémentation satisfait le même protocole et que les clients en aval sont respectueux du protocole.
• Auditabilité : La chaîne de preuves fournit un mécanisme pour reconstruire les décisions d'admission et vérifier qu'un artefact a été admis sur la base de contraintes spécifiques, plutôt que sur la confiance en le générateur.

Importance et positionnement

L'article positionne le PDD comme une évolution nécessaire pour l'ère du « Logiciel 2.0 » et de la synthèse automatisée. Son importance réside dans l'unification de traditions disparates — méthodes formelles, tests, application de politiques et provenance — en un seul modèle d'admission.

• Distinction par rapport aux travaux existants : Contrairement au développement « Schema-first » (qui se concentre sur la structure), au TDD (qui se concentre sur des exemples fonctionnels) ou à la politique en tant que code (qui opère souvent au moment de l'exécution), le PDD élève le bundle de protocole au rang d'artefact principal gouvernant conjointement la structure, le comportement, l'autorité opérationnelle et la preuve d'admission.
• Philosophie : La thèse centrale est « Le code est transitoire ; le protocole est souverain ». À mesure que les coûts d'implémentation tendent vers zéro, le produit intellectuel de l'ingénierie logicielle devient l'ensemble des contraintes formelles définissant le comportement admissible et la preuve que ces contraintes ont été respectées.
• Travaux futurs : L'article esquisse un agenda empirique pour tester le PDD contre des références SDD et TDD, en se concentrant sur la réduction de l'ambiguïté, la fiabilité de la régénération, la substituabilité, la surcharge de validation et l'efficacité de la gouvernance. Il suggère des orientations futures incluant des registres de protocoles réutilisables, la synthèse automatisée de protocoles et une intégration plus profonde avec des outils de vérification formelle.

En résumé, le PDD propose une couche de gouvernance pour l'ingénierie logicielle automatisée où la « loi » est le protocole, et les « citoyens » sont des implémentations générées admises uniquement par la preuve vérifiable de conformité.