Les méthodes formelles et l’avenir de la programmation

• Les méthodes formelles sont des outils qui permettent de prouver qu’un logiciel satisfait les propriétés attendues, et la diffusion du codage par agents modifie l’évaluation coûts-bénéfices
• Jane Street estimait autrefois que, hors de quelques cas particuliers, les méthodes formelles offraient une valeur trop faible au regard de leur coût, mais met désormais en place une équipe dédiée
• seL4 a nécessité 25 années-personnes pour vérifier 8 700 lignes de code C, avec environ 23 lignes de preuve et une demi-journée-personne de vérification par ligne de code
• Le code généré par les agents reste éloigné de la qualité requise pour une mise en production, et les méthodes formelles deviennent importantes comme moyen de réduire le goulet d’étranglement de la vérification et de fournir un feedback fort aux agents
• Jane Street estime que, grâce à son contrôle profond sur le langage et à l’existence d’une communauté de programmeurs déjà prête, il y a de la place pour faire progresser OxCaml et les approches orientées preuve ensemble

---

Les méthodes formelles et l’avenir de la programmation

• Jane Street affirme depuis 25 ans qu’au niveau de l’organisation, l’entreprise ne s’intéresse pas aux méthodes formelles, mais cette position n’est désormais plus la sienne
• L’entreprise accorde depuis longtemps de l’importance à la puissance des outils permettant d’écrire un meilleur code et un code plus fiable, et considère les systèmes de types comme une forme légère de méthode formelle qui a apporté de grands bénéfices
• En dehors de cas particuliers, notamment la synthèse matérielle, elle jugeait que le coût des méthodes formelles était trop élevé pour convenir à la plupart des logiciels
• seL4 est un micronoyau vérifié formellement et une réalisation majeure, mais la vérification de 8 700 lignes de code C a demandé 25 années-personnes
  • Environ 23 lignes de preuve étaient nécessaires pour chaque ligne de code, et la vérification d’une ligne demandait environ une demi-journée-personne
• Pour des cas à fort enjeu et à spécification relativement claire, comme un micronoyau critique pour la sécurité, cette approche peut avoir de la valeur
• Elle ne semblait pas adaptée à la plupart des logiciels, ni même aux logiciels les plus importants de Jane Street
• L’arrivée du codage par agents a changé ce jugement, et le scepticisme vis-à-vis du potentiel des méthodes formelles s’est transformé en attente positive
• Jane Street est en train de créer une équipe méthodes formelles et espère en faire un outil de construction logicielle aussi largement utile que les systèmes de types sophistiqués

Pourquoi ce changement d’avis

• Le codage par agents bouscule de plusieurs façons le rapport coûts-bénéfices historique des méthodes formelles
• Cela ne signifie pas que les agents peuvent, à eux seuls et de façon arbitraire, construire des preuves difficiles, mais les modèles apportent une aide importante et permettent à davantage de personnes d’utiliser les outils de manière productive
• Comme l’usage des méthodes formelles devient plus simple qu’auparavant, il vaut la peine de réexaminer le calcul coût/efficacité du passé

• Le goulet d’étranglement de la vérification devient plus important

  • Les modèles écrivent de mieux en mieux du code utile, mais il existe encore un écart important entre le code généré par les modèles et le code réellement publiable
  • Les modèles sont étonnamment performants pour atteindre un objectif donné, mais pas assez solides pour maintenir ou améliorer la qualité d’une base de code au passage
  • Le code produit par les agents s’améliore, mais il tend à être excessivement complexe, plein de bugs étranges et de cas limites, et à ne pas respecter les invariants essentiels de la base de code
  • Les humains doivent consacrer beaucoup de temps à vérifier si le code produit par les agents est d’une qualité suffisante
  • Les méthodes formelles peuvent réduire cette charge de vérification et rendre le processus de revue plus efficace

• Les agents deviennent meilleurs grâce au feedback

  • Les agents tirent parti du feedback, à la fois lors de l’entraînement par apprentissage par renforcement et lors de leur utilisation pour coder
  • Les méthodes formelles constituent une forme de feedback puissante capable d’améliorer la faculté des agents à résoudre des problèmes difficiles
  • Les tests restent très précieux, et ils peuvent encore être améliorés à l’aide du test basé sur les propriétés et du fuzzing
  • Les tests seuls ne suffisent pas, et il existe des limites intrinsèques à leur capacité à couvrir l’espace des états qu’un programme peut explorer
  • Dans l’expérience de programmation avec OxCaml, les agents tirent un grand bénéfice des garanties universelles fournies par le système de types
  • Si le système de types peut empêcher les data races, alors il peut éliminer les data races
  • Si des types bien conçus rendent impossibles les vulnérabilités de type cross-site scripting, elles peuvent être éliminées d’une manière difficile à obtenir avec de simples tests
  • Les types atténuent le goulet d’étranglement de la vérification et fournissent un meilleur feedback lorsqu’on programme avec des agents
  • L’usage de techniques de preuve plus puissantes pourrait permettre des progrès supplémentaires

Pourquoi ici

• Le monde entier réfléchit à ce que les agents signifient pour l’avenir de la programmation, et de nombreuses startups cherchent aussi à combiner méthodes formelles et agents
• Jane Street peut contrôler en profondeur le langage qu’elle utilise, ce qui lui permet de l’ajuster pour le rendre plus adapté aux approches orientées preuve
• Plusieurs directions sont possibles
  • Il est possible d’intégrer au système de types des spécifications modulaires de propriétés
  • On peut ajouter au niveau des types des contraintes sur des éléments comme la propriété et la mutabilité afin de faciliter certaines preuves
  • On peut intégrer directement des techniques de preuve dans le langage

• Une communauté de programmeurs prête

  • Jane Street dispose d’une communauté de programmeurs prête à adopter ce type de techniques
  • Pour ceux qui travaillent sur les langages de programmation, il est souvent plus difficile de faire adopter dans le travail réel de meilleures idées de programmation que d’inventer ces idées
  • Chez Jane Street, il est fréquent que des utilisateurs se plaignent que de nouvelles fonctionnalités de système de types, prometteuses mais inhabituelles, n’arrivent pas assez vite
  • De nombreuses personnes y ont déjà le bagage nécessaire pour tirer parti de ces techniques, et l’attention portée à la production de résultats corrects et de logiciels de haute qualité y est déjà bien ancrée
  • Une base d’utilisateurs active et très demandeuse donne la liberté de tenter à la fois des améliorations de court terme et une vision de long terme
  • Les améliorations de court terme peuvent avoir un impact relativement rapide
  • La vision de long terme correspond à des objectifs plus ambitieux pouvant être atteints sur plusieurs années
  • Les enseignements tirés des essais à court terme peuvent servir à construire vers les objectifs de long terme

• Relation avec les outils externes

  • Jane Street n’ignore pas le travail effectué à l’extérieur et puise attentes et inspiration dans le travail de plusieurs communautés de langages de programmation
  • Parmi les outils concernés figurent Lean, Dafny, Rocq, Agda, Iris
  • L’entreprise cherche des moyens d’intégrer OxCaml à certains de ces outils afin de tirer parti d’une excellente infrastructure déjà existante
  • Elle estime aussi qu’il existe des avantages propres que l’on ne peut obtenir qu’en traitant simultanément le langage et les techniques de preuve

Rejoindre l’équipe

• Jane Street recrute sur les méthodes formelles à London et New York
• Les entretiens pour ces postes et la constitution de l’équipe n’en sont encore qu’à leurs débuts
• Il reste énormément de travail à faire, et l’entreprise cherche des personnes pour rejoindre l’équipe

Complément

• Les modèles ont encore besoin d’aide et de guidage humains lorsqu’ils traitent des preuves complexes
• Les programmeurs humains peuvent avoir des idées sur la raison pour laquelle un système fonctionne et sur la manière de le prouver à un niveau élevé
• La plupart des programmeurs ne savent pas comment encoder une idée de preuve d’une façon qui satisfasse un système de preuve donné
• Les modèles peuvent automatiser une grande partie du travail répétitif dans les détails techniques de la rédaction des preuves et apporter l’expertise nécessaire
• Des échappatoires comme Obj.magic peuvent permettre de contourner des contraintes au niveau des types
• En suivant et en interdisant ces exceptions dans la majorité du code, on peut se rapprocher très fortement de garanties universelles
• Les méthodes formelles peuvent rendre explicites les raisons pour lesquelles l’usage de telles échappatoires est effectivement sûr

[GN⁺]

Commentaires sur Hacker News

• Il y a plusieurs décennies, j’ai travaillé sur la preuve de correction, et à l’époque le système automatisait davantage les preuves que beaucoup de systèmes apparus ensuite
  Les parties faciles étaient prises en charge par le simplificateur Oppen-Nelson, le tout premier solveur SAT, et les parties difficiles par le démonstrateur Boyer-Moore, qui utilisait des heuristiques et des lemmes antérieurs. La partie difficile pour l’humain consistait à suggérer au démonstrateur des lemmes qu’il pourrait tenter puis réutiliser dans les preuves suivantes
  Les systèmes apparus ensuite semblaient moins automatisés, et à mon avis les méthodes formelles se sont égarées parce qu’elles sont devenues trop formalistes par rapport aux besoins réels. Du point de vue de quelqu’un qui voulait du code sans bug pour des projets commerciaux, j’avais l’impression que les projets académiques subissaient un biais de mathématiciens, privilégiant des notations concises pour les articles et des analyses avec peu de cas
  En pratique, il faut beaucoup de travail automatisé et peu d’intuition. Des gens brillants ont continué à inventer de nouvelles logiques, comme la logique modale ou la logique temporelle, pour éviter la verbosité des preuves sur papier, mais cela n’a pas beaucoup aidé. La vérité fondamentale de ce domaine, c’est que la plupart des théorèmes sont assez ordinaires
  Comme le disent les gens de Jane Street, le fait de pouvoir contrôler le langage est un énorme avantage. Les assertions de vérification doivent être intégrées au langage de programmation ; si elles sont enfouies dans des commentaires, une autre syntaxe ou des fichiers séparés, cela ajoute du travail inutile. J’aime bien voir Jane Street pousser dans cette direction
  J’ai travaillé là-dessus bien trop tôt, il y a plus de 40 ans ; à l’époque, reconstruire l’arithmétique depuis zéro avec le démonstrateur Boyer-Moore prenait environ 45 minutes de calcul, alors qu’aujourd’hui cela prend moins d’une seconde
  https://archive.org/details/manualzilla-id-5928072/page/n3/m...

  • En tant que personne qui travaille sur les méthodes formelles depuis longtemps, j’ai un peu de mal à être d’accord avec l’idée que les nouvelles logiques n’aident pas. Les logiques industrielles sont pratiques et permettent d’exprimer de manière très concise des propriétés sophistiquées que les systèmes doivent satisfaire
    La logique occupe en informatique et en génie logiciel une place comparable à celle du calcul différentiel en physique, en mécanique ou en génie civil. Des choses comme LTL ou, plus récemment, la logique de séparation ont été d’énormes percées
    La popularité assez large de TLA+ en est la preuve, et le model checking est très pratique. Ce qui est intéressant aujourd’hui, c’est que des méthodes formelles plus lourdes, en particulier la démonstration de théorèmes, pourraient devenir assez abordables pour être utilisées même dans les logiciels systèmes généralistes
    Écrire une spécification formelle pour une fonction, puis la synthétiser et en prouver la correction à l’aide d’un hybride SAT/SMT, démonstrateur de théorèmes et LLM pourrait bientôt devenir la norme
    On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
    From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
  • Dans les spécifications formelles, le fait qu’un humain puisse les interpréter et les écrire va devenir vraiment important
    Ce qui m’inquiète, c’est l’apparition de mathématiques difficiles à déchiffrer, protégées par de petits groupes d’initiés. Différentes notations ésotériques ne seront pas compatibles entre elles, et en comprendre une n’aidera pas forcément beaucoup à en comprendre une autre. La plupart des gens finiront par n’écrire que des phrases en anglais impossibles à vérifier correctement
    Pire encore, on pourrait demander aux machines de formaliser leurs propres phrases, puis participer à un théâtre de la vérification sans comprendre ni le formalisme ni les preuves, avant de faire semblant d’être surpris quand tout explose
  • Je me demande si vous avez regardé Ada/SPARK. Si oui, je serais curieux de savoir si cela correspond à votre intuition de ce à quoi les choses devraient ressembler
    On progresse lentement vers l’intégration de ce type de capacités pour les parties que le système de types ne traite pas rapidement, donc le point de vue de gens qui ont déjà emprunté cette voie m’intéresse

• Très bien. Ces derniers mois, j’ai migré en Scala 3 vers des types expressifs, afin que les types embarquent de plus en plus de preuves à la compilation. Je n’utilise pas de macros, même si quelques-unes peuvent être utiles
  Cette approche ne semble pas seulement aider à réduire le problème de la prolifération des tests agentiques, elle semble aussi empêcher les agents de retomber dans des méthodes de travail de faible qualité. En particulier, elle évite cette accumulation de substantifs où l’agent crée un nouveau type mono-cas pour tout, même lorsqu’il devrait raisonnablement généraliser
  Je pense que ce qui accélérera le codage agentique de bonne qualité, ce sont des outils qui ressemblent aux méthodes formelles, y compris des langages dotés de systèmes de types puissants
  Par types expressifs, j’entends des techniques qu’on ne voudrait pas forcément introduire dans une base de code classique si l’équipe n’est pas déjà à l’aise avec la programmation au niveau des types. Autrement dit, il faut une équipe pour qui les types de genre supérieur et les fonctions de type ne sont pas des étrangetés, mais des briques de base
  Les agents sont généralement meilleurs en « mathématiques » que la plupart des développeurs sur le plan des connaissances, et souvent meilleurs même que des développeurs imbibés de théorie des catégories. En plus, si l’on considère qu’ils ont une patience « infinie » en conversation, ils enseignent plutôt bien
  Personnellement, j’ai demandé à Codex de convertir quelques petites preuves de loisir dans le style Lean, et cela a été très facile. Je ne dirais pas que c’est exact à 100 %, et pour vérifier plus sérieusement il faudrait que j’apprenne davantage Lean 4, mais il semble au moins repérer les pièges classiques des preuves. L’avenir des méthodes formelles me rend très enthousiaste

• Il semble que l’idée soit de déplacer la valeur humaine vers la vérification, puisque la Gen AI produit énormément de code. Je me demande parfois ce qu’est vraiment la programmation.
  Quand l’anglais n’est pas sa langue maternelle, apprendre la programmation est déjà en soi un grand défi. Pour comprendre la documentation anglaise non traduite, il faut s’appuyer sur la traduction automatique, et les ressources disponibles dans ma langue ont 5 à 6 ans de retard.
  Maintenant qu’il est impossible de relire des dizaines de milliers de lignes de code générées par l’IA, on voit apparaître des discussions sur l’établissement de règles absolues, comme des preuves mathématiques. En lisant cet article, j’ai pensé au borrow checker de Rust. En pratique, après avoir utilisé Rust quelques fois, on voit souvent les gens prendre de mauvaises habitudes en cherchant des astuces pour contourner le borrow checker.
  Quand la rigueur mathématique devient excessive, les gens finissent par chercher des voies de contournement. Les programmeurs peu formés comme moi y sont particulièrement enclins.
  J’ai l’impression que ce type d’approche finira par produire du code écrit uniquement pour des réponses formalisées très spécifiques. Une fois standardisé de cette façon, je ne suis pas sûr qu’il puisse encore répondre aux besoins humains.
  Ces tentatives de programmation défensive sont très bien, mais, pour reprendre ma propre expression, j’ai envie de faire de la programmation offensive. C’est une manière de travailler qui accepte le risque, mais corrige et déploie vite, avec l’idée qu’au fil du temps le résultat deviendra suffisamment bon.
  Bien sûr, dans des secteurs établis comme Jane Street, où la précision est cruciale et le périmètre de travail bien défini, l’approche de cet article est adaptée. Ils disposent de suffisamment de données pour modéliser correctement les besoins du marché.
  Mais pour un perdant social comme moi, qui continue à se déplacer pour trouver sa mine d’or et gagner de l’argent, ce genre de méthodologie ressemble à un luxe. Les activités existantes, avec une modélisation mature, doivent être continuellement optimisées par des spécialistes très qualifiés, et je sais qu’en pratique il est impossible de suivre cette demande. C’est pourquoi je cherche des endroits où la modélisation n’est pas structurée, mais je ne sais pas si cette approche pourrait y fonctionner aussi.

  • Il faut voir ça du point de vue de Jane Street. C’est une société de trading à haute fréquence, qui échange des actions et des produits financiers par millions, voire peut-être par dizaines de millions.
    Là-bas, il n’y a pas de « on corrigera plus tard ». Quand on aura compris ce qui s’est mal passé, on aura peut-être déjà perdu des milliards.
    Donc l’approche offensive peut fonctionner dans des domaines non essentiels.
    D’ailleurs, on utilise déjà un peu partout des approches défensives. Python, Java et d’autres ont des garbage collectors, et en ce sens on vérifie bien que le code s’exécute comme prévu.
    Je me demandais quand la vérification formelle commencerait à apparaître, mais passer du stade où l’on se soucie des détails d’implémentation à celui où l’on décrit scientifiquement et mathématiquement le problème est quelque chose de naturel.
  • J’aime bien l’expression « programmation offensive ». Cela dit, ce paradigme est déjà l’état par défaut du secteur.
    Avec la Gen AI, le coût de la programmation défensive a beaucoup baissé, tandis que le coût de la vérification humaine a fortement augmenté. À l’inverse, les méthodes formelles rendent la vérification moins coûteuse, mais introduisent un gros surcoût d’implémentation : il faut écrire des spécifications, des types, des preuves, et tordre l’implémentation pour la faire entrer dans un cadre rigide.
    Or la Gen AI peut automatiser ce travail pénible. Les deux sont faits l’un pour l’autre.
  • Si vous dépendez de la traduction automatique pour lire de la documentation anglaise non traduite, c’est un peu hors sujet, mais je recommande fortement d’apprendre l’anglais.
    Cela demande un peu d’effort, mais éliminer ce surcoût de traduction permanent vous aidera énormément.
  • Je suis d’accord sur le fait que cette méthodologie est un luxe. L’article le reconnaît lui-même, et Jane Street est une organisation particulièrement bien préparée pour tirer profit de cette approche.
  • Il est naturel que Jane Street publie un tel texte parce que cela les concerne directement, et il est tout aussi naturel que cela ne s’applique pas de manière générale à toute la programmation.
    En revanche, je ne vois pas bien le lien entre ce point et le fait de se qualifier soi-même de « perdant social », ou de dire que l’on ne suit pas ce genre de pratiques dans sa carrière.

• Je m’amuse récemment avec des idées connexes, et ce qui m’a surpris, c’est à quel point les modèles de pointe, en particulier ChatGPT-5.5, parviennent bien à compléter certaines preuves manuelles dans Roqc, l’ancien assistant de preuve Coq.
  Les preuves ne sont pas toujours élégantes, mais ChatGPT parvient souvent, en quelques minutes et en 10 à 100 itérations, à produire des démonstrations qui me prendraient bien plus longtemps, alors même que j’ai une expérience certes limitée mais réelle avec les assistants de preuve, ainsi qu’une expérience de domaine assez importante sur le type de lemmes à démontrer.
  Ce qui rend cela intéressant dans le contexte de ce court article, c’est que cela remet en cause les hypothèses de base du fonctionnement de certains outils de méthodes formelles. Frama-C, Ada/SPARK et d’autres se concentrent sur la génération d’obligations de preuve que des outils comme CVC5 ou Z3 peuvent résoudre automatiquement ; en cas d’échec, on bascule vers l’alternative assez pénible de la preuve manuelle dans Roqc.
  Le flux habituel consiste à découvrir qu’une obligation est « difficile », c’est-à-dire qu’elle n’est pas résolue automatiquement, puis à reconfigurer l’ensemble des lemmes auxiliaires et des assertions visibles au point du code où cette obligation est générée, afin de la rendre « facile », voire à modifier le code lui-même.
  Cela a du sens dans un monde où une preuve Roqc coûte deux fois plus cher : elle est difficile à écrire pour un humain, et son coût de maintenance varie fortement quand le code et les preuves périphériques changent.
  Mais si une preuve Roqc devient une « résolution automatique avec l’IA dans la boucle », alors cet écart de coût disparaît. On peut alors écrire des preuves comme on écrit du code, en mettant la clarté lisible par les humains en priorité absolue, et en reléguant très loin derrière l’optimisation pour le compilateur ou le démonstrateur. Je n’ai pas encore complètement assimilé toutes les implications, mais je trouve cela assez fascinant.

  • Quand les exigences changent et qu’on se retrouve dans une situation impossible à prouver, quelle est la probabilité que l’IA modifie le code et les exigences pour rendre la preuve plus facile ?
    Je n’ai jamais travaillé sur les preuves, mais il m’est déjà arrivé de voir une IA modifier les tests eux-mêmes, au lieu de corriger le code pour qu’il fasse bien ce que je voulais — à savoir faire passer à la fois les anciens tests et les nouveaux — quand je lui disais : « après la modification, ce test échoue ».
  • C’est proche de mon expérience aussi, mais moi j’ai choisi Lean. C’était davantage lié aux fonctionnalités que je voulais construire.
    J’ai hâte de voir la suite.
  • Quand vous dites que ChatGPT parvient à produire des preuves Roqc en quelques minutes et 10 à 100 itérations, je me demande comment vous savez si la preuve elle-même est correcte.

• Chaque fois que je lis sur les spécifications formelles, j’ai l’impression que c’est « écrire les mêmes tests d’une autre manière », voire pire, « écrire la même implémentation d’une autre manière »
  Le fait de l’écrire deux fois peut sans doute aider à repérer des erreurs, mais si une spécification formelle peut avoir les mêmes bugs qu’un test ou qu’une implémentation, je ne vois pas bien ce qu’elle a de spécial
  Le problème de fond, c’est que pour prouver formellement qu’un programme fait quelque chose, il faut définir ce « quelque chose » de manière très précise. Au final, cela revient de fait à réécrire le test ou l’implémentation
  Cela fait des années que je regarde ce sujet par intermittence, avec la sensation persistante de rater quelque chose, sans savoir quoi. Quelqu’un pourrait-il m’expliquer ?

  • Comme l’a dit Dijkstra dans sa célèbre formule, « les tests de programmes peuvent montrer la présence de bugs, mais jamais leur absence »
    Le défaut des tests, c’est qu’on ne peut tester que les comportements que l’on soupçonne de poser problème. Pour corriger de manière préventive des comportements dont on ignorait même qu’ils pouvaient mal tourner, il faut des outils plus atypiques dans la boîte à outils. Le fuzz testing est un début dans cette direction, et la vérification formelle en est un autre
    Bien sûr, la qualité de ces outils dépend de la qualité du modèle formel exhaustif que l’on écrit, capable d’autoriser les comportements voulus et d’interdire ceux qu’on ne veut pas, et dans de nombreux domaines nous sommes encore étonnamment loin du compte
  • La grande différence, c’est que les méthodes formelles permettent d’utiliser le quantificateur universel pour tout
    Par exemple, avec un test unitaire, on peut écrire « foo('abc') renvoie une chaîne sans espace de fin »
    Mais avec des méthodes formelles, on peut prouver que « pour toute entrée x, foo(x) renvoie une chaîne sans espace de fin »
    C’est un exemple trivial, mais on peut imaginer quelque chose de plus complexe comme « pour tout programme P, compile(P) se comporte comme P »
    Bien sûr, il faut définir ce que signifie « se comporte comme »
  • Je n’en fais pas pour le logiciel, mais dans la conception d’ASIC et de FPGA, les spécifications en méthodes formelles permettent à des outils comme les solveurs SAT de déterminer si la conception cible satisfait la spécification
    On spécifie des propriétés de la conception, puis l’outil teste celle-ci de diverses façons pour vérifier si ces propriétés peuvent être violées
    Par exemple, pour un système qui contrôle des feux de circulation, on peut spécifier la propriété selon laquelle deux voies qui se croisent ne peuvent pas être au vert en même temps, ni dans un certain intervalle de temps
    L’outil vérifie cela par exploration exhaustive et peut montrer la trace de code qui viole la propriété
  • C’est plus que simplement « écrire les mêmes tests d’une autre manière ». Chaque test est en général indépendant, ou devient ingérablement gros, et on doit évaluer l’exhaustivité d’un ensemble de tests par des formes de recouvrement relativement grossières, comme la couverture de branches
    Un système de types prouvé statiquement permet de vérifier à l’avance que chaque composant s’accorde avec tous les autres. Il ne s’agit pas seulement de dire « ce test passe », mais de garantir qu’une fois combinés, « tous ces tests forment un ensemble raisonnable et cohérent », et d’empêcher qu’un modèle incohérent soit implémenté dans le code
    C’est un peu comme prendre l’exigence de Rust selon laquelle match doit couvrir exhaustivement toutes les branches possibles et l’étendre à l’échelle de toute la base de code
    Il est vrai que cela ne vous protégera pas d’une erreur logique ou théorique fondamentale. Mais on peut être surpris de voir à quel point c’est plus robuste, par exemple, que la combinaison du système de types de Haskell, de tests fonctionnels ad hoc et de tests de propriétés. Cet ensemble constitue déjà globalement un cadre solide, mais la cryptographie formellement prouvée vise un niveau bien plus élevé
  • La différence décisive se situe entre des tests particuliers et une preuve exhaustive. Si l’on ne pense pas à tester un cas limite, il passe inaperçu. Avec un bon modèle, on peut savoir qu’il existe et le corriger avant le déploiement
    C’est particulièrement précieux dans les situations de concurrence, de systèmes distribués et de multithreading. Les race conditions et les interblocages sont très difficiles à tester et à raisonner, tout comme les questions du type « A, B et C peuvent-ils se produire dans l’ordre A, C, B ? »
    La maturation de ce domaine suivra probablement à peu près cette trajectoire. D’abord, les LLM accéléreront fortement l’apprentissage et l’usage des méthodes formelles, même s’ils se limitent au départ à une sorte de vérification a posteriori, un « deuxième essai »
    Ensuite, on passera à une automatisation où le LLM vérifiera « le code d’implémentation a changé, mais cela semble-t-il casser le modèle ? ». Cela restera non déterministe, mais ce sera probablement bien mieux que de demander à un humain de revoir quelque chose qui ne change qu’occasionnellement
    Enfin, le vrai saut consistera à faire passer au niveau supérieur les outils du type « n’écrivez que la spécification formelle et générez l’implémentation ». Il existe déjà plusieurs projets de génération de code de ce genre, mais la plupart ne sont pas encore totalement mûrs au niveau qu’attendent les entreprises. Et si des outils LLM pouvaient accélérer les 1 à 2 années de travail manuel nécessaires pour adapter l’un d’eux à un besoin précis ?

• L’article précédent de Kleppmann https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... mérite aussi le détour, et il faut évidemment se demander si ce qu’on peut mettre dans un système de types ou dans un linter ne devrait pas simplement y être mis
  J’espère qu’il émergera des approches plus simples à utiliser. Parmi les outils cités dans l’article, dafny et iris semblent les plus proches d’un usage industriel. Je crois savoir qu’Amazon S3 a aussi un historique d’usage interne de TLA
  Mais je n’ai pas encore vu dans ce domaine l’équivalent d’un TypeScript : quelque chose qui s’intègre naturellement aux outils existants, fonctionne comme une abstraction sans coût et que les gens préfèrent sincèrement à l’ancienne manière de faire
  Même utiliser des linters personnalisés reste assez pénible. golangci-lint est une base de code douloureuse, et je n’ai pas essayé semgrep, mais son moteur de règles m’a paru intimidant. Je n’ai pas encore non plus utilisé d’API AST qui me plaise vraiment

• Cet éloge du raisonnement déductif, autrement dit des « méthodes formelles », passe toujours à côté de sa limite fondamentale : dans quelle mesure les axiomes et les définitions correspondent-ils réellement au domaine visé
  C’est le même problème que dans la formule « En théorie, il n’y a pas de différence entre la théorie et la pratique. En pratique… ». J’imagine que Jane Street continuera à maintenir une grande base de code où l’objectif du code est de mettre en œuvre des algorithmes déterministes, donc avec une correspondance 1:1. Beaucoup de développeurs travaillent dans ce type de domaine, mais des millions n’y sont pas. C’est le cas de la plupart des UI, de la plupart des travaux exploratoires, etc.
  Parallèlement aux méthodes formelles, il existe aussi un courant qui cherche à définir les critères d’acceptation avec une très haute résolution, sans passer par une approche logique ou mathématique. Ce courant affronte au moins le problème de la correspondance, mais il ne le résout pas dans la plupart des cas où la carte n’est pas le territoire.
  La page de résultats de recherche Google dispose d’un framework interne d’optimisation extrêmement évolué, mais a-t-elle vraiment atteint l’optimum ? Un prototype bricolé à la hâte pour capturer une idée floue aurait-il pu mieux montrer la voie ? À ce type de questions, on répond le mieux en regardant non pas l’intérieur du système, mais l’extérieur qu’il sert

  • Les méthodes formelles sont précisément faites pour des domaines dont la sémantique est bien définie
    Les circuits logiques, les composants CPU fortement soumis à la vérification formelle, les kernels, les protocoles, les parseurs, les compilateurs, la cryptographie, les frameworks de sécurité, les primitives de concurrence, etc., tirent de grands bénéfices de la vérification
  • En pratique, la plupart des UI finissent par se ramener à des machines à états, ce qui se prête très bien à la vérification formelle
    Pour aller plus loin, le texte de Hillel Wayne est un bon point de départ : https://www.hillelwayne.com/formally-specifying-uis/
  • La page de résultats Google elle-même n’est pas bien définie, mais probablement plus de 90 % du code sous-jacent l’est
    Et dans certains cas, on peut apprendre même si le résultat n’est pas bien défini, donc ce n’est pas seulement une question de s’asseoir pour réfléchir à ce qui pourrait avoir du sens

• En tant que personne un peu intéressée par la conception et l’implémentation des langages de programmation, cette phrase m’a vraiment marqué. « Pour la plupart des gens qui travaillent sur les langages de programmation, la partie facile consiste à imaginer des idées nouvelles et meilleures pour améliorer la programmation. La partie difficile consiste à convaincre quelqu’un d’utiliser réellement ces idées dans son travail »
  Je suis totalement d’accord. Même quand il y a un bénéfice, il existe une limite à la quantité d’étrangeté qu’on peut introduire dans un nouveau langage
  Mais les agents IA ne ressentiront probablement pas une forte résistance face à des idées radicalement nouvelles en conception de langages. Je réfléchis depuis quelque temps à la manière dont la conception des langages de programmation pourrait évoluer après l’arrivée de l’IA agentique
  Quand on a beaucoup moins à se soucier de l’adoption, il sera très intéressant de voir quelles nouvelles idées on pourra inventer pour améliorer les langages de programmation
  https://steveklabnik.com/writing/the-language-strangeness-bu...

• Je travaille sur l’application des méthodes formelles aux tests de sécurité applicative, et je pense que la même approche peut aussi s’appliquer à la vérification de la logique métier
  Pour cela, nous utilisons la taint analysis. C’est une approche de méthodes formelles assez bien établie, mais elle n’a pas encore été largement adoptée sur le terrain à cause de la complexité des flux de données dans les vraies bases de code
  Étendre les méthodes formelles au-delà du pattern matching sur l’AST et des simples vérifications de types est un travail vraiment difficile. Il a fallu des années de R&D pour atteindre un niveau où la taint analysis peut suivre en quelques minutes les flux de données interprocéduraux dans de vraies bases de code et trouver des vulnérabilités profondément enfouies
  Si cela vous intéresse, vous pouvez voir le projet : https://github.com/seqra/opentaint

• Il y a environ 18 mois, je suis devenu accro à l’usage des types avec les LLM, et je me suis mis sérieusement à lean4 il y a environ 6 à 8 mois. Désormais, je n’envisage même plus d’utiliser une assistance IA pour le développement logiciel sans un socle de preuves CIC avec une FFI C/C++ pratique, donc relié de fait à à peu près tout
  Nous avons interdit tout ce qui va de JSON à Python, et nous avons même réécrit nix pour qu’il dispose d’un compilateur. Presque tout ce que nous utilisons subit non seulement des tests par propriétés et plusieurs fuzz tests poussés à la limite, mais possède aussi au minimum une preuve lean4 pilotant les tests par propriétés via un lien .olean. Quand nous avons le temps, nous prouvons même l’exhaustivité de tout le domaine et testons aussi cette propriété
  Tout ce qui est rapide est généré depuis lean4, ce qui permet de passer à côté des débats C++/Rust. Il y a un avantage quand un bug C++ est en réalité un bug dans le code lean4, mais cela peut aller dans les deux sens
  C’est un changement majeur, et je ne blâme pas ceux qui restent sceptiques en entendant « vous interdisez JSON et Python ? ». Mais nous avons inspecté des millions de lignes de cette manière, et IA + système formel représente un saut bien plus grand que de passer de l’absence d’IA à l’IA avec Python. D’après notre expérience, la seconde approche ne progresse pas de manière monotone, alors que la première progresse presque toujours de façon monotone
  On peut faire des choses assez audacieuses. Voici une preuve formelle de calculs tensoriels polyédriques du type de ceux que modélisent ISL et CuTe, et cela permet de faire du swizzling et du tiling sur l’appareil avec mdspan de C++23 tout en prouvant que c’est correct. En revanche, cet exemple n’illustre pas très bien un argument à la L'Hôpital sur la couverture : https://github.com/b7r6/mdspan-cute
  Le résultat est vraiment rapide, et il l’est dès le premier essai
  https://straylight.software/assets/lambda-hierarchy.svg

  • Placer Agda et Idris 2 sous CIC rend le diagramme de la hiérarchie lambda trompeur, même dans la lecture la plus bienveillante
  • Je serais donc curieux de savoir quel logiciel a été produit, et pourquoi il est utile