La correction dans un monde agentique§

Les agents vont écrire la plupart du code que nous déployons. L'époque où l'on écrit du code à la main touche à sa fin plus tôt que je n'y suis prêt.

Comme tous les changements de paradigme, celui-ci engendre beaucoup de déni, d'anxiété, d'incertitude, de remise en question, d'hubris et un sentiment général de dislocation. Quand le chaos règne, je trouve utile de chercher des parallèles et des cadres de référence crédibles pour donner un sens à ce qui se passe.

Dans ce billet, je soutiendrai que des techniques qui semblaient autrefois exotiques, démesurées ou « ce qu'utilisent les gens qui peaufinent depuis trop longtemps » vont bientôt devenir le minimum requis. Je tracerai un parallèle avec le passage de l'assembleur aux langages de haut niveau, puis je soutiendrai que nous faisons face structurellement au même problème aujourd'hui, sauf sur une chronologie comprimée.

Enfin, je rejoindrai le camp de ceux qui disent : les méthodes formelles, le property-based testing, les spécifications mécaniquement vérifiées doivent devenir les outils que nous saisissons maintenant. L'économie a basculé en leur faveur et, franchement : c'est probablement le niveau d'abstraction sur lequel nous devons commencer à nous concentrer pour garder un contrôle positif sur la sortie des agents.

De l'assembleur aux langages de haut niveau§

Quand les langages de plus haut niveau sont arrivés, on disait aux gens d'arrêter d'écrire de l'assembleur. La transition a pris du temps. Les compilateurs avaient des bugs qui généraient du code incorrect. L'assembleur écrit à la main était — et est souvent encore — plus rapide que ce que les compilateurs émettent. La transition a tout de même eu lieu, sur des décennies, avec des artisans qui marchaient sur la corde raide en gardant leurs compétences en assembleur tout en adoptant les langages de plus haut niveau. À mesure que les compilateurs s'amélioraient, presque tout le monde a fini par basculer. Les langages de plus haut niveau ont commencé à développer leurs propres astuces — compilation JIT, ramasse-miettes, generational heaps — techniquement possibles en assembleur mais devenues pratiques seulement au niveau d'abstraction supérieur. Le schéma était à peu près :

• Phase 0 : Tout le monde écrit de l'assembleur. Quelques personnes étranges utilisent des langages de haut niveau, jouent avec divers runtimes — Prolog, systèmes symboliques, choses considérées comme marginales.
• Phase 1 : Les gens commencent à écrire en langages de haut niveau, perçus comme peu sérieux par les autres. Les anciens s'inquiètent que les nouveaux venus ne sachent pas coder. Ils argumentent qu'il faudrait vérifier par échantillonnage la sortie des compilateurs pour s'assurer de sa correction, qu'on devrait tous maintenir nos compétences en assembleur.
• Phase 2 : Une grande partie de l'effort de recherche en langages de programmation est consacrée à prouver que le code généré par les compilateurs est correct, ou du moins raisonnablement correct dans la plupart des cas.
• Phase 3 : Les gens écrivent principalement en langages de haut niveau. Les compilateurs et interpréteurs sont largement corrects. Plus personne ne croit qu'écrire dans un langage de haut niveau soit un choix curieux. Il est parfaitement acceptable de ne pas connaître l'assembleur et d'être un ingénieur compétent.

Cela a pris environ cinquante ans, freiné par l'offre de chercheurs en langages de programmation, l'appétit commercial pour investir dans ce travail, et le fait que prouver ces choses est en fait difficile et lent. Pour chaque génération de rêveurs déjantés¹ poussant des idées folles sur l'avenir, les praticiens contemporains se grattaient la tête, légèrement dédaigneux et sceptiques. Et pour l'essentiel, les rêveurs (biais du survivant, je sais) ont fini par avoir raison. Les langages de haut niveau, les représentations quasi en anglais, et le « plus-personne-ne-lit-d'assembleur » sont devenus la norme.

Je soutiens que nous sommes au même point parallèle aujourd'hui. Cinquante ans d'arc compressés en quelques mois.

Le langage naturel§

Nous sommes montés d'un niveau de plus. Nous écrivons désormais en langages EHL (even-higher-level) : le langage naturel. Nous attendons des agents LLM qu'ils traduisent l'EHL en HL (Go, Rust, Python, TypeScript). Et nous n'avons pas vraiment confiance dans la sortie.

En tant qu'artisans, nous nous comportons de la même manière que lors du dernier saut d'ordre de grandeur :

• nous exigeons que les gens vérifient la sortie des agents LLM
• nous ne faisons pas confiance à la sortie par défaut
• nous nous inquiétons pour les jeunes qui n'auront pas l'occasion d'apprendre à coder (en langages HL)
• le concept de « laisser les LLM écrire le code » passe de marginal à raisonnablement accepté
• les puristes du EHL en pointe font des trucs bizarres que tout le monde trouve déconcertants²

La bonne nouvelle, c'est que, de la même manière que passer de l'assembleur au HL nous a donné des cycles mentaux disponibles pour développer de nouveaux concepts (JIT, GC, generational heaps), passer du HL à l'EHL nous donne des cycles disponibles — et accessoirement, plus de main-d'œuvre — pour relever le niveau d'exigence sur la correction. La question est : comment faire confiance au fait que l'EHL se compile en HL valide ? Comment résoudre les inquiétudes de correction issues du codage agentique ?

Méthodes de génie logiciel§

Au cours des deux ou trois dernières décennies, le TDD et la discipline qui l'entoure ont soutenu — sur différents registres — que les tests sont un artefact de première classe dans la génération de logiciel.³ Dans certains domaines, c'est allé trop loin (« n'écris pas une seule ligne de code sans test ! »), mais je pense que le pendule revient. C'est soudainement à nouveau pertinent, parce que si vous ne clouez pas les agents au sol avec un véritable harnais de tests, ils vont écrire du non-sens plausible et s'en aller en sifflotant. Il y a un an, je ne m'astreignais pas à « n'écris pas de code sans un test d'abord », mais aujourd'hui je tiens absolument mes agents à ce standard.

Mais le TDD n'a jamais été l'alpha et l'oméga des tests. Depuis les années 1940, on sait que les propriétés des programmes peuvent être prouvées. Tony Hoare a publié « An Axiomatic Basis for Computer Programming » en 1969. Pendant des décennies, on a dit que c'était « impraticable pour du vrai logiciel ». Une chimère académique.

Le test unitaire typique parcourt un chemin à travers l'état du programme.⁴ Tests « golden », table tests, tests unitaires, tests d'intégration — variations de la même idée. Ils prouvent que ce qui est connu est connu. Ils ne prouvent jamais rien à propos des inconnus.

Le property-based testing⁵ (PBT) effectue des marches aléatoires à travers l'espace d'état — en générant des plages plausibles de valeurs d'entrée et en vérifiant que le programme ne viole jamais de propriétés spécifiques. Exprimable essentiellement à l'identique en Go (rapid), Rust (proptest), TypeScript (fast-check).⁶ Chacun tire des centaines ou milliers de vecteurs aléatoires et réduit les échecs à des contre-exemples minimaux. Strictement plus fort qu'un test unitaire.

En Go, cela ressemble à ceci :

func TestSortIsIdempotent(t *testing.T) {
    rapid.Check(t, func(t *rapid.T) {
        v := rapid.SliceOf(rapid.Int()).Draw(t, "v")
        once := append([]int(nil), v...)
        sort.Ints(once)
        twice := append([]int(nil), once...)
        sort.Ints(twice)
        require.Equal(t, once, twice)
    })
}

L'invariant : le tri est idempotent.

Trier une tranche déjà triée ne la change pas : . Ce test s'exécute des milliers de fois avec diverses entrées et garantit que l'invariant est toujours vrai. Quand il échoue, il réduit le domaine d'entrée à la plage minimale qui reproduit la violation de l'invariant.

Le PBT a sa propre histoire de débuts à la marge⁷. John Hughes et Koen Claessen ont publié « QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs » à ICFP 2000. Pendant des années, c'était traité comme « les gens de Haskell sont bizarres », jusqu'à ce que cela se répande dans tous les langages grand public.

Pour une vraie preuve de correction, il faut des méthodes formelles. Historiquement réservées aux seuls systèmes les plus critiques, en raison du coût prohibitif. Mais pour ce qui est spécifié, on a une garantie bien plus forte que « le programme est probablement correct, je suppose ». Une spécification TLA+⁸ est une machine à états, un invariant, et un théorème que le model checker vérifie à travers tous les états atteignables — pas seulement une marche, toutes les marches. C'est la différence entre un test et une preuve.

Comme le PBT, TLA+ a eu son propre parcours étrange. Leslie Lamport l'a développé au début des années 1990. Un exercice académique de niche pendant deux décennies — jusqu'à ce que Newcombe et al., 2015 documente comment AWS a utilisé TLA+ pour trouver des bugs dans DynamoDB, S3, et EBS avant de les déployer. Un écart de vingt ans entre la publication et la percée industrielle.⁹

Des techniques qui paraissent gaspilleuses, de niche, ou absurdes à l'an zéro deviennent souvent rationnelles une fois que le niveau d'abstraction environnant et l'économie ont bougé. Le GC était gaspilleur sur un PDP-1 ; sur un serveur avec 64 Go de RAM, ce n'est même plus une question. La technique n'a pas changé. Le coût de ne pas l'utiliser, si.

La compression du temps est la nouvelle variable. L'arc de l'article de Hoare de 1969 à AWS-sur-TLA+ a pris environ quarante-cinq ans. Le prochain arc ne devrait pas prendre quarante-cinq — ni vingt, ni même cinq. Les agents font des ravages dans le code HL en ce moment même. Les spécifications sont le prochain refuge sûr¹⁰, et nous devrions y speedrunner. Les gens se sont largement accordés sur le fait qu'écrire des spécifications produit solides en markdown est la manière dont nous prompt-engineerons notre chemin vers le succès agentique. Et la nouvelle marge va au-delà.

Oui, une spécification produit solide est le début. Mais ensuite la programmation industrielle exige plus que ça et que des vibes de « fais-moi confiance, frère ». Nous devons faire le travail que les praticiens du HL ont fait en garantissant que la sortie est correcte pour le périmètre qui nous importe, d'une manière qui maintienne la supervision humaine sans nous noyer dans une mer de code que nous ne pouvons pas réviser. Nous ne pourrons pas réviser tout ce code. Nous ne pourrons pas nous permettre de ne pas produire tout ce code. C'est là la tension. Donc nous devons battre en retraite vers le haut et commencer à nous concentrer non plus seulement sur les spécifications produit mais aussi à les coupler à des preuves formelles, du PBT basé sur des invariants, des modèles mécaniquement vérifiables, toute la panoplie. Nous devons battre en retraite loin de l'écriture et de la revue de code HL et aller vers la rédaction de ces contrats d'assurance : rédiger du code de niveau encore supérieur (EHL).

L'économie vient juste de basculer§

Trois choses viennent de se produire en même temps.

1. La productivité a fait un bond. Les agents représentent un changement d'ordre de grandeur dans la vitesse à laquelle le code s'écrit. Si vous avez travaillé avec une bonne boucle d'agent pendant une semaine, vous l'avez ressenti directement.

2. Le risque de qualité a fait un bond avec elle. Les agents hallucinent, dérivent, écrivent du code plausible mais subtilement faux. Sans compensation, la qualité du code régresse à mesure que les agents prennent davantage le clavier.

3. Les méthodes qui compensent le point 2 viennent de devenir bon marché.

Les méthodes formelles n'ont jamais été chères en calcul¹¹. Elles étaient chères en attention humaine. Dans un domaine proche du mien (rédiger des opérateurs Kubernetes), l'article Anvil rapportait un ratio preuve-sur-code d'environ 4,5x pour qu'un humain rédige les preuves et les itère jusqu'à clôture. Ça fait beaucoup de preuves. C'est pour ça que « utiliser TLA+ sur tout » n'a jamais gagné en adoption industrielle malgré son fonctionnement en principe depuis trente ans.

Mais cette taxe est payée par un travailleur différent désormais. Les vérificateurs sont déterministes, vérifiés mécaniquement, vert ou rouge sans ambiguïté. Quand la preuve ne se ferme pas, le vérificateur vous dit exactement quelle conjecture échoue sur quel état. C'est le flux de travail dans lequel les agents excellent : boucle de rétroaction serrée, signal clair, itérer jusqu'à convergence.

Et les agents ne s'ennuient pas.

Les techniques précédemment limitées par la patience humaine sont désormais limitées par le calcul, qui est bon marché. Balancer du matériel sur le problème, c'est toute l'histoire ici.

Donc le calcul s'inverse. Nous payons une fraction de notre gain de productivité pour sur-indexer sur la correction, et nous en sortons net positifs — plus de portée, qualité supérieure qu'avant. La correction doit devenir le minimum requis maintenant, non pas parce que nous sommes puristes, mais parce que les maths tournent en notre faveur quand nous le faisons et contre nous quand nous ne le faisons pas.

Faire confiance au code agentique§

Les techniques dont nous avons besoin existent déjà — elles attendaient juste un basculement du modèle de coût, et ce basculement vient de se produire.¹² Donc je postule, maintenant :

• Pour la logique cœur de tout programme non trivial — machines à états, invariants qui doivent tenir, parties où « presque correct » n'est pas correct — utilisez les méthodes formelles, ou essayez. Pour des preuves au niveau du logiciel avec assistance LLM : Dafny, Verus, ou Lean (Creusot et Kani sont des choix Rust complémentaires). Pour la conception de systèmes distribués : P ou TLA+.
• Pour le gros du reste — partout où il y a un espace d'entrée significatif — utilisez le property-based testing par défaut. Nous devrions probablement investir dans l'outillage de mutation testing pour garantir que les agents n'écrivent pas de tests inutiles et trompeurs.
• Pour la couverture de régression et de personas en happy-path — gardez les tests traditionnels, mais soyez honnêtes : ce ne sont pas vos tests de correction. Ce sont vos tests de présentation. « Ça fait ce que ce test dit que ça fait ».
• Pour le spec-driven development — rédigez aussi des spécifications formelles pour les parties porteuses. Coût marginal faible, bénéfice grand.

Ceci ne sera pas optionnel longtemps. Les méthodes existent. Le coût vient de chuter. Le gain de productivité issu des agents à la fois paie l'investissement et l'exige.

Notre refuge sûr — pour l'instant§

Le royaume HL est en cours de colonisation par les agents. On ne les combat pas sur leur terrain — on bat en retraite vers le haut, vers la couche au-dessus du code : langage naturel, spécifications produit, spécifications formelles, invariants, modèles de domaine, personas. Les choses qui étaient autrefois fragiles (spécifications produit informelles, user stories) et les choses qui étaient autrefois coûteuses (méthodes formelles, motifs de tests avancés) sont toutes deux porteuses désormais, pour la même raison — c'est ainsi que nous restons lisibles à nous-mêmes et gardons un levier d'exécution sur ce que font les agents en bas, au pays HL.

Les compétences qui comptent sont celles qui permettent d'opérer cette couche : écrire des user stories assez bien pour qu'elles contraignent réellement, dériver des modèles de domaine, identifier les invariants, décider où tester vs. vérifier vs. prouver, concevoir la spécification assez serrée pour qu'un agent ne puisse pas s'en tirer par une pirouette. Si vous ne savez pas faire ça — écrire des user stories, dériver des modèles de domaine, trouver des invariants, assembler le tout en couches d'abstraction qui valent la peine d'être testées — votre déjeuner est fini, et quelqu'un a mangé votre sandwich.

1. 1
   Grace Hopper a conçu FLOW-MATIC (1955-59), a livré un compilateur qui lisait des énoncés de forme anglaise face au « les ordinateurs ne peuvent pas comprendre l'anglais ». John Backus a mené FORTRAN chez IBM (1957) ; la prêtrise de l'assembleur disait que le code compilé ne pouvait pas égaler la performance écrite à la main, le 704 a démontré le contraire. John McCarthy a conçu LISP (1958) et a livré le ramasse-miettes en production pour la première fois ; le GC a été rejeté comme impraticable pour le « vrai » travail pendant des décennies. Dijkstra, « Go To Considered Harmful » (1968) — la programmation structurée comme marginale avant de devenir incontournable. Robin Milner a conçu ML (1973) avec inférence de types, « les programmes bien typés ne peuvent pas mal tourner » — exotisme académique alors, ancêtre de conception de tout langage typé aujourd'hui. L'arc — FORTRAN ('57) à C ('72) à C++ ('85) à Java ('95) à Go ('09) à Rust ('10) — était freiné par l'offre de chercheurs, l'appétit commercial, et le fait que prouver ces choses est difficile.
2. 2
   Steve Yegge (Gas Town, Gas City), Geoffrey Huntley (ralph loops), le commentaire en cours de Simon Willison.
3. 3
   Kent Beck, TDD: By Example (2002) ; Fowler, Refactoring (1999) ; McConnell, Code Complete (2e éd. 2004) ; Dan North, « Introducing BDD » (2006) ; Gojko Adzic, Specification by Example (2011).
4. 4
   Les tests basés sur des exemples échantillonnent l'espace d'entrée en un point fixe. Les métriques de couverture mesurent ce qui a été parcouru, pas ce qui est correct. La phrase de Dijkstra à OTAN 1969 est canonique : « Le test de programme peut être utilisé pour montrer la présence de bugs, mais jamais pour montrer leur absence ! » (rapport, élaboré dans EWD249). La garantie « toutes les marches » vient du model checking — exploration exhaustive des états atteignables jusqu'à une borne.
5. 5
   Membres de la famille : metamorphic testing — relations entre les sorties d'entrées liées (ML, code scientifique) ; differential testing — deux implémentations, mêmes entrées, comparer (compilateurs, refactorisations, portages) ; stateful/model-based PBT — séquences d'opérations contre un modèle (rapid.StateMachine, proptest-state-machine, quickcheck-state-machine) ; concolic execution (KLEE, SAGE) ; mutation testing — mesurer la force des tests. Le fuzzing est la variante à générateur adverse. Aucune d'elles ne peut prouver qu'un programme est correct sauf pour les plus triviaux — la combinatoire explose vite.
6. 6
   Là où je pense que le codage agentique se consolide. TypeScript : les types structurels font de la vérification à la compilation l'achat de correction le moins cher à la frontière humain-vers-agent. Rust : Verus et le système de types rendent le proof-carrying code faisable ; la taxe ergonomique qui ralentissait les humains, les agents la paient facilement. Go : la boucle compile/vet/test rapide compte quand on pilote un agent ; vet/staticcheck/race-detector/fuzzing sont matures.
7. 7
   John Hughes et Koen Claessen, « QuickCheck » (ICFP 2000). Pendant des années traité comme « les gens de Haskell sont bizarres », jusqu'à ce que cela se répande dans tous les langages grand public : rapid (Go), proptest (Rust), fast-check (JS/TS), hypothesis (Python).
8. 8
   Une minuscule spécification TLA+ :

   ---- MODULE Counter ----
   VARIABLES count
   
   Init == count = 0
   Next == count' = count + 1
   
   Spec == Init /\ [][Next]_count
   
   NonNegative == count >= 0
   THEOREM Spec => []NonNegative
   ====
   

9. 9
   Xavier Leroy / CompCert, milieu des années 2000 — compilateur C formellement vérifié, utilisé aujourd'hui dans l'aérospatial et la crypto. L4.verified / seL4 (2009) — premier micro-noyau d'OS formellement vérifié. RustBelt (POPL 2018) — le système de types de Rust prouvé sain. Verus et Anvil (OSDI '24, Best Paper) — contrôleurs Kubernetes formellement vérifiés en Rust, actuellement en phase « curiosité académique ».
10. 10
    Ce refuge sûr ne dure pas éternellement non plus. La même compression qui a dévoré le HL viendra pour la couche de spécification — des agents dérivant des spécifications à partir d'objectifs, les vérifiant les uns contre les autres. D'ici là, nous sommes plus proches de la Culture d'Iain M. Banks que de l'industrie logicielle actuelle, et la question devient « comment les humains vivent-ils leur meilleure vie pendant que l'IA s'échine sans relâche ».
11. 11
    Le coût par exécution peut être non trivial — les exécutions TLC, les vérifications de preuves Verus, les campagnes de fuzzing mâchent du CPU. L'économie tient toujours : le logiciel, c'est « compile/vérifie une fois, livre plusieurs fois » — coût marginal de distribution proche de zéro, selon « Why Software Is Eating the World » d'Andreessen. Balancez du matériel sur la vérification, optimisez pour la ressource rare (l'attention humaine).
12. 12
    Le prochain changement d'ordre de grandeur n'arrive pas dans 20-30 ans ; il arrive dans 2-3. Ne vous endormez pas trop longtemps sur vos lauriers. Apprenez à vivre sur la courbe.