La correction dans un monde agentique§

Les agents vont écrire la plus grande partie du code que nous déployons. L'époque où l'on écrivait du code à la main touche à sa fin, plus vite que la plupart d'entre nous ne sommes prêts à l'accepter.

Je vais soutenir que les techniques que nous avons historiquement traitées comme exotiques — méthodes formelles, property-based testing, spécifications vérifiées mécaniquement — doivent devenir des table-stakes dès maintenant, parce que l'économie a basculé en leur faveur.

De l'assembleur aux langages de haut niveau§

Quand les langages de plus haut niveau sont apparus, on a dit aux gens d'arrêter d'écrire de l'assembleur. La transition a pris du temps. Les compilateurs avaient des bugs qui produisaient une génération de code incorrecte. L'assembleur écrit à la main était — et reste souvent — plus rapide que ce qu'émettent les compilateurs. La transition a tout de même eu lieu, sur des décennies, avec des artisans qui passaient à travers le chas de l'aiguille 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, garbage collection, tas générationnels — techniquement possibles en assembleur mais qui ne sont devenues pratiques qu'au niveau d'abstraction supérieur. Le schéma était à peu près :

• Phase 0 : Tout le monde écrit de l'assembleur. Quelques originaux utilisent des langages de haut niveau, jouent avec divers runtimes — Prolog, systèmes symboliques, choses considérées marginales.
• Phase 1 : Les gens commencent à écrire dans des langages de haut niveau, jugés peu sérieux par les autres. Les anciens craignent que les nouveaux venus ne sachent pas coder. Ils soutiennent qu'on devrait vérifier ponctuellement la sortie des compilateurs pour s'assurer de sa correction, et que nous devrions tous entretenir 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 majoritairement dans des langages de haut niveau. Les compilateurs et interpréteurs sont en grande partie corrects. Plus personne ne croit qu'écrire dans un langage de haut niveau soit un choix bizarre. 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, rythmé par l'offre de chercheurs en langages de programmation, par l'appétit commercial pour investir dans ce travail, et par le fait que prouver ces choses est intrinsèquement difficile et lent. Chaque génération a absorbé les hérétiques de la précédente¹.

Je soutiens que nous sommes maintenant dans la même position parallèle, en version compressée. Cinquante ans de trajectoire, compressés à quelques mois.

Langage naturel§

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

En tant qu'artisans, nous nous comportons de la même manière qu'au précédent saut d'ordre de grandeur :

• nous exigeons que des humains 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 « laisser les LLM écrire du code » passe du statut de marginal à raisonnablement accepté
• les puristes à la pointe du EHL font des trucs bizarres que les autres trouvent 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, tas générationnels), passer du HL à l'EHL nous donne des cycles disponibles — et accessoirement, plus de bras — pour rehausser la barre côté correction. La question est : comment faire confiance au fait que l'EHL compile vers du HL valide ? Comment résoudre les inquiétudes de correction liées au code agentique ?

Méthodes du génie logiciel§

Au cours des deux à trois dernières décennies, le TDD et la discipline qui l'entoure ont soutenu — sur différents registres — que le test est un artefact de premier ordre dans la production de logiciel.³ Les zélotes sont allés trop loin et le balancier a fait son retour. Le sujet redevient soudain pertinent, parce que si vous ne coincez pas les agents avec un véritable harnais de tests, ils écriront des âneries plausibles et s'en iront en sifflotant.

Mais le TDD n'a jamais été l'alpha et l'oméga du test. Depuis les années 1940, nous savons que les propriétés des programmes peuvent être prouvées. Tony Hoare a publié « An Axiomatic Basis for Computer Programming » en 1969. « Impraticable pour du vrai logiciel », disait-on, pendant des décennies.

Le test unitaire typique parcourt un chemin à travers l'état du programme.⁴ Tests golden, tests tabulaires, tests unitaires, tests d'intégration — variations sur le même thème. Ils prouvent que ce qui est connu est connu. Ils ne prouvent jamais rien sur les inconnus.

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

En Go, ça 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 différentes entrées et garantit que l'invariant est toujours vrai. Quand il échoue, il réduit le domaine d'entrée à l'intervalle minimal qui reproduit la violation de l'invariant.

Le PBT a sa propre histoire d'hérétiques⁷. John Hughes et Koen Claessen ont publié « QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs » à ICFP 2000. Pendant des années, ç'a été traité comme un truc-de-bizarres-qui-font-du-Haskell, jusqu'à ce que ça se diffuse à tous les langages grand public.

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

TLA+ a sa propre histoire de marginaux. Leslie Lamport l'a développé au début des années 1990. Exercice académique de niche pendant deux décennies — jusqu'à ce que Newcombe et al., 2015 documentent comment AWS a utilisé TLA+ pour trouver des bugs dans DynamoDB, S3 et EBS avant de les déployer. Vingt ans d'écart entre la publication et la percée industrielle. Le schéma ne cesse de se répéter.⁹

Le schéma n'est pas « les marginaux finissent toujours par avoir raison ». Il est plus étroit et plus utile : les techniques qui paraissent gaspilleuses, de niche ou absurdes à l'année zéro deviennent souvent rationnelles une fois que le niveau d'abstraction et l'économie environnants ont bougé. Le GC était du gaspillage 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, lui, a changé.

La compression est la nouvelle variable. La trajectoire allant de l'article de Hoare en 1969 à AWS-sur-TLA+ a pris environ quarante-cinq ans. La trajectoire suivante ne devrait pas prendre quarante-cinq — ni vingt, ni même cinq. Les agents se déchaînent dans le code HL en ce moment même. Les specs sont le prochain refuge¹⁰, et nous devrions y speedruner.

L'économie vient 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 agentique pendant une semaine, vous l'avez ressenti directement.

2. Le risque qualité a fait un bond en même temps. 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 plus de place sur le clavier.

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

Les méthodes formelles n'ont jamais été coûteuses en calcul¹¹. Elles étaient coûteuses en attention humaine. L'article d'Anvil rapporte un ratio preuve/code d'environ 4,5x — pour qu'un humain écrive les preuves et les itère jusqu'à leur clôture. C'est pourquoi « utiliser TLA+ sur tout » n'a jamais remporté d'adoption industrielle, malgré le fait que ça fonctionne en principe depuis trente ans.

Cette taxe est désormais payée par un travailleur différent. Les vérificateurs sont déterministes, vérifiés par la machine, sans ambiguïté vert ou rouge. Quand la preuve ne se clôt pas, le vérificateur vous dit exactement quelle conjecture échoue sur quel état. C'est exactement le flux de travail auquel les agents sont le mieux adaptés : 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 maintenant limitées par le calcul, qui est bon marché.

Donc la donne s'inverse. Nous payons une fraction de notre gain de productivité pour miser excessivement sur la correction, et nous en ressortons gagnants au final — portée plus large, qualité plus élevée qu'avant. La correction doit devenir une table-stake dès maintenant, non pas parce que nous serions des puristes, mais parce que le calcul joue en notre faveur quand on le fait et contre nous quand on ne le fait pas.

Faire confiance au code agentique§

Les techniques dont nous avons besoin existent déjà — elles n'attendaient qu'un basculement du modèle de coût, et ce basculement vient d'avoir lieu.¹² Donc je pose, maintenant :

• Pour la logique centrale de tout programme non trivial — machines à états, invariants qui doivent tenir, parties où « presque juste » n'est pas juste — utilisez les méthodes formelles. Pour des preuves au niveau logiciel avec assistance LLM : Dafny, Verus ou Lean (Creusot et Kani sont des choix complémentaires côté Rust). Pour la conception de systèmes distribués : P ou TLA+.
• Pour la majeure partie du reste — partout où il existe un espace d'entrée significatif — utilisez le property-based testing par défaut.
• Pour la couverture des régressions et des personas en happy path — gardez les tests traditionnels, mais soyez honnêtes : ce n'est pas votre test de correction. C'est votre test de présentation.
• Pour le spec-driven development — écrivez aussi une spec TLA+ pour les parties porteuses. Coût marginal faible, gain élevé.

Ce n'est plus optionnel. Les méthodes existent. Le coût vient de chuter. Le gain de productivité apporté par les agents paie l'investissement et l'exige à la fois.

Notre refuge — pour l'instant§

Le royaume HL est en cours de colonisation par les agents. Nous ne combattons pas cela sur leur terrain — nous nous replions vers le haut, à la couche au-dessus du code : langage naturel, specs produit, specs formelles, invariants, modèles de domaine, personas. Les choses qui étaient autrefois fragiles (specs produit informelles, user stories) et les choses qui étaient autrefois coûteuses (méthodes formelles, patterns de tests avancés) sont désormais toutes les deux porteuses, pour la même raison — elles sont la manière dont nous restons lisibles à nos propres yeux et conservons un levier d'application sur ce que les agents font en bas, au pays du HL.

Les compétences qui comptent sont celles qui vous 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 des invariants, décider où tester versus vérifier versus prouver, concevoir la spec assez serrée pour qu'un agent ne puisse pas la contourner en douce. Si vous ne savez pas faire tout cela — é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 terminé, et quelqu'un a mangé votre sandwich.

1. 1
   Grace Hopper a conçu FLOW-MATIC (1955-59), livré un compilateur qui lisait des instructions en forme d'anglais malgré le « les ordinateurs ne peuvent pas comprendre l'anglais ». John Backus a dirigé FORTRAN chez IBM (1957) ; le clergé de l'assembleur disait que le code compilé ne pouvait pas égaler les performances écrites à la main, le 704 a démontré le contraire. John McCarthy a conçu LISP (1958) et livré le garbage collection en production pour la première fois ; le GC a été écarté 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 une table-stake. Robin Milner a conçu ML (1973) avec inférence de types, « les programmes bien typés ne peuvent pas mal tourner » — curiosité académique à l'époque, ancêtre conceptuel de tout langage typé d'aujourd'hui. La trajectoire — FORTRAN ('57) vers C ('72) vers C++ ('85) vers Java ('95) vers Go ('09) vers Rust ('10) — a été rythmée 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 continu 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 à l'OTAN en 1969 est canonique : « Les tests de programmes peuvent servir à montrer la présence de bugs, mais jamais à montrer leur absence ! » (rapport, développé dans EWD249). La garantie « toutes les marches » vient de la vérification de modèle — exploration exhaustive des états atteignables jusqu'à une borne.
5. 5
   Membres de la famille : tests métamorphiques — relations entre les sorties d'entrées apparentées (ML, code scientifique) ; tests différentiels — deux implémentations, mêmes entrées, comparer (compilateurs, refactorisations, portages) ; PBT avec état / basé sur un modèle — séquences d'opérations contre un modèle (rapid.StateMachine, proptest-state-machine, quickcheck-state-machine) ; exécution concolique (KLEE, SAGE) ; tests de mutation — mesurer la robustesse des tests. Le fuzzing est la variante à générateur adverse. Aucun 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 code agentique se consolide. TypeScript : les types structurels font de la vérification à la compilation l'achat le moins coûteux côté correction à la frontière humain-vers-agent. Rust : Verus et le système de types rendent le code à preuve embarquée faisable ; la taxe ergonomique qui a freiné les humains est ce que les agents paient sans difficulté. Go : la boucle rapide compile/vet/test compte quand on pilote un agent ; vet/staticcheck/détecteur de course/fuzzing sont matures.
7. 7
   John Hughes et Koen Claessen, « QuickCheck » (ICFP 2000). Pendant des années traité comme un truc-de-bizarres-qui-font-du-Haskell, jusqu'à ce que ça se diffuse à tous les langages grand public : rapid (Go), proptest (Rust), fast-check (JS/TS), hypothesis (Python).
8. 8
   Une minuscule spec 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 en aérospatiale et en cryptographie. L4.verified / seL4 (2009) — premier micro-noyau de système d'exploitation 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 de « curiosité académique ».
10. 10
    Ce refuge ne dure pas éternellement non plus. La même compression qui a mangé le HL viendra pour la couche des specs — des agents dérivant les specs à partir des objectifs, les vérifiant les unes contre les autres. À ce moment-là, nous serons plus proches de la Culture d'Iain M. Banks que de l'industrie logicielle d'aujourd'hui, et la question deviendra « comment les humains vivent-ils leur meilleure vie pendant que l'IA trime ».
11. 11
    Le coût par exécution peut être non négligeable — les exécutions TLC, les vérifications de preuves Verus, les campagnes de fuzzing mâchent du CPU. L'économie tient quand même : le logiciel, c'est « compile/vérifie une fois, expédie de nombreuses fois » — coût marginal de distribution proche de zéro, selon le « 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 reposez pas trop longtemps sur vos lauriers. Apprenez à vivre sur la courbe.