Comment devenir un meilleur programmeur en faisant de petites preuves dans sa tête

• Pour devenir un meilleur programmeur, il est important de prendre l’habitude de construire de petites preuves mentalement au moment d’écrire du code
• La monotonicité, l’immuabilité, les préconditions et postconditions, ainsi que les invariants, sont des concepts clés dans ces mini-preuves
• Concevoir en tenant compte de l’étendue de l’impact des modifications de code sur l’ensemble du système (isolation, pare-feu) aide fortement à réduire la complexité et les risques
• L’induction permet de prouver pas à pas la correction des fonctions ou structures récursives
• Cette manière de penser se développe par la pratique et l’habitude, et l’entraînement aux démonstrations mathématiques comme à la résolution de problèmes d’algorithmes aide beaucoup

---

Introduction et idée centrale

• Avec l’expérience, l’auteur a naturellement pris l’habitude de « se représenter de petites preuves » afin d’améliorer la justesse et la rapidité de son code
• Le processus qui consiste à vérifier et raisonner mentalement sur le comportement attendu pendant qu’on code demande de l’entraînement, mais une fois maîtrisé, il améliore nettement la qualité du code
• La manière précise de le faire importe moins que le fait de s’exercer de différentes façons pour trouver celle qui vous convient

Monotonicité (Monotonicity)

• La monotonicité (monotonicity) désigne la propriété d’une fonction ou d’un code qui ne progresse que dans une seule direction
• L’auteur prend comme exemple le checkpointing : les étapes de travail n’avancent que vers l’avant et ne reviennent pas en arrière pour réexécuter un travail déjà terminé
• Dans l’exemple des LSM trees comparés aux B-trees, un LSM tree accumule généralement l’espace utilisé, qui ne diminue qu’au moment de la compaction
• Quand la monotonicité est garantie, on peut naturellement exclure ou prédire certaines parties d’un état ou d’un résultat complexe
• L’immuabilité (immutability) est une idée proche : une valeur définie une fois ne change jamais, ce qui élimine certaines possibilités d’évolution de l’état

Préconditions et postconditions (Pre- and post-conditions)

• Les préconditions (pre-condition) et postconditions (post-condition) sont des assertions qui doivent impérativement être vraies avant et après l’exécution d’une fonction
• Suivre explicitement ces conditions lors de l’écriture d’une fonction aide à la réflexion logique et aux tests
• Définir clairement les postconditions permet de dériver plus facilement des cas de tests unitaires
• Ajouter dans le code des assertions qui vérifient ces conditions et provoquent un arrêt précoce dans les situations imprévues améliore la prévisibilité et la sûreté
• Il arrive qu’il soit difficile d’attribuer à une fonction des préconditions ou postconditions claires ; le simple fait de le constater est déjà instructif

Invariants

• Les invariants sont des propriétés qui doivent toujours rester vraies, quelles que soient les circonstances, avant, pendant et après l’exécution du code
• L’équation comptable de la comptabilité en partie double en est un exemple représentatif (total crédit = total débit)
• Si l’on décompose l’ensemble du code en petites étapes et que l’on prouve que chacune préserve l’invariant, on garantit l’intégrité de l’ensemble
• Pour maintenir les invariants, on peut utiliser des listeners ou des méthodes de cycle de vie (comme les constructeurs/destructeurs en C++, ou useEffect dans React)
• La vérification des invariants est bien plus simple quand les changements sont limités ou que les chemins d’exécution sont simples

Isolation

• L’un des éléments essentiels d’un bon logiciel consiste à ajouter ou modifier des fonctionnalités sans déstabiliser le système existant
• Il faut identifier le « rayon d’impact » (blast radius) des changements de code et créer des « pare-feu » structurels pour minimiser la propagation de leurs effets
• À partir de l’exemple du service Nerve, l’auteur présente une approche qui consiste à délimiter clairement la frontière entre le query planner et le query executor, puis à concevoir les changements de façon qu’ils ne traversent pas cette frontière
• Empêcher la propagation inutile des changements facilite la validation et la maintenance, tout en améliorant la stabilité
• Cela rejoint aussi la philosophie de l’OCP (Open-Closed Principle) : étendre les fonctionnalités sans modifier le comportement existant

Induction

• De nombreux programmes contiennent des fonctions récursives ou des structures récursives, et l’induction est un outil puissant pour formaliser le raisonnement à leur sujet
• Pour prouver étape par étape le comportement et la correction d’une fonction récursive, il faut vérifier séparément le cas de base (base case) et l’étape d’induction (inductive step)
• L’auteur prend comme exemple la simplification de nœuds dans une structure d’AST (arbre syntaxique) et montre comment un raisonnement inductif à chaque étape permet de prouver le maintien des invariants et le bon fonctionnement
• Une fois le raisonnement inductif bien intégré, écrire et vérifier du code récursif devient beaucoup plus intuitif et simple
• Il est intéressant de comparer cette approche à une tentative de vérification globale (holistic), non inductive, pour voir laquelle paraît la plus naturelle

La proof-affinity comme indicateur de qualité

• L’auteur défend l’idée qu’un bon code est un code dans lequel on peut faire de petites preuves dans sa tête
• Quand le code possède des structures comme la monotonicité, l’immuabilité, des conditions claires, une décomposition en invariants, des frontières de type pare-feu et le recours à l’induction, il devient effectivement plus facile à prouver, et donc de meilleure qualité
• Si un code est difficile à comprendre et ardu à vérifier, cela suggère qu’un refactoring ou une révision de sa structure est nécessaire
• L’auteur propose ici le terme proof-affinity plutôt que celui de « prouvabilité »
• La proof-affinity n’est pas le seul facteur de qualité logicielle, mais c’est un puissant facilitateur pour comprendre, étendre, tester et maintenir le code

Comment progresser

• Cette manière de penser logique doit être suffisamment pratiquée pour devenir naturelle et inconsciente
• Écrire fréquemment des démonstrations (mathématiques) et développer sa capacité de raisonnement logique est indispensable
• La résolution de problèmes d’algorithmes (cours EdX de Stanford, Leetcode, etc.) constitue aussi un excellent terrain d’entraînement ; se concentrer sur des problèmes qui exigent une implémentation rigoureuse et un raisonnement de type démonstratif, plutôt que de simples astuces, permet de mieux progresser
• Il est important de s’entraîner à s’approcher de la bonne réponse du premier coup, plutôt que de corriger le résultat à répétition
• En ancrant ainsi ces habitudes, on peut nettement améliorer la conception de systèmes logiques et la qualité du code

[GN⁺]

Avis Hacker News

• Il existe un exemple simple mais étonnant qui correspond exactement à ce sujet : la recherche binaire. Il y a bien des variantes gauche/droite, mais si on ne réfléchit pas aux invariants de boucle, c’est très difficile de l’implémenter correctement. Cet article explique l’approche par invariant ainsi qu’un exemple de code Python correspondant. Jon Bentley, l’auteur de Programming Pearls, avait demandé à des programmeurs d’IBM d’implémenter une recherche binaire ordinaire, et 90 % d’entre eux ont produit du code bogué. L’erreur la plus fréquente était de tomber dans une boucle infinie. À l’époque, il fallait aussi prévenir soi-même les dépassements d’entiers, donc c’est compréhensible dans une certaine mesure, mais le pourcentage reste surprenant

  • C’est en voyant cela que j’ai commencé à utiliser la recherche binaire comme question d’entretien. Environ 2/3 de candidats pourtant réputés n’arrivaient pas à produire en moins de 20 minutes une implémentation qui fonctionne correctement. En particulier, beaucoup tombaient dans des boucles infinies sur des cas pourtant faciles. Ceux qui réussissaient l’implémentaient rapidement. Une des causes du problème, c’est que beaucoup ont appris avec une mauvaise interface. Même l’explication de Wikipédia dit « initialiser L à 0 et R à n-1 », donc avec une borne droite incluse. En pratique, pour la plupart des algorithmes sur les chaînes, il vaut mieux une borne supérieure exclusive, donc R = n. J’aimerais vraiment tester cette hypothèse expérimentalement : faire écrire l’algorithme à beaucoup de gens avec différents prototypes de fonction et différentes valeurs initiales, puis comparer combien de bugs apparaissent avec une borne supérieure inclusive, exclusive, ou une approche par longueur

  • En réalité, la recherche binaire est presque l’exemple type le plus délicat en matière de gestion d’indices. Avec l’algorithme de partition de Hoare, c’est l’un des algorithmes de base les plus difficiles à coder correctement sans se tromper

  • Pour tester, j’ai demandé à Claude Sonnet d’écrire un code Python de recherche binaire sans bug

  def binary_search(arr, target):
      left = 0
      right = len(arr) - 1
      while left <= right:
          mid = left + (right - left) // 2
          if arr[mid] == target:
              return mid
          elif arr[mid] < target:
              left = mid + 1
          else:
              right = mid - 1
      return -1
  

  J’ai aussi vérifié différents cas de test sur un tableau d’exemple

  • Sachant que les bugs de recherche binaire sont célèbres comme faux « best practice », j’avais voulu relever le défi d’inclure dans un livre une première implémentation sans bug. Je l’ai rédigée avec énormément de soin, mais il y avait quand même un bug, ce qui me fait encore sourire. Heureusement, grâce au système de retour anticipé de Manning, j’ai pu le corriger avant l’impression

  • Pour implémenter une recherche binaire gauche/droite, je procède toujours en mémorisant « la meilleure valeur trouvée jusque-là ». C’est la même idée que lower_bound et upper_bound en C++. Avec une structure while (l < r), on calcule le point médian, on vérifie la position courante et on ajuste l’intervalle en conséquence. Par exemple, pour upper_bound, on remonte la borne gauche, et pour lower_bound, on abaisse la borne droite. Je refaisais du leetcode après longtemps et j’avais le cerveau embrumé, donc le format est peut-être un peu bancal

• J’ai l’impression d’avoir découvert un concept proche de celui-ci il y a longtemps, en cours de master. Vers la fin de ma licence, j’ai commencé à passer les examens de maths uniquement au stylo. Je ne sais pas exactement pourquoi, mais mes notes étaient toujours bonnes : je résolvais tout d’un trait en ayant déjà complètement déroulé la démonstration dans ma tête avant d’écrire. Ça réduisait énormément les erreurs. Je code aussi de cette façon : je commence après avoir conçu les choses de manière assez aboutie dans ma tête

• Pour devenir un meilleur programmeur, il faut prendre l’habitude d’écrire de petites preuves autour du code Les tests et les définitions de types en sont justement des exemples J’aborde surtout les choses dans l’ordre suivant : d’abord les tests, ensuite les types, et enfin le code L’idéal est de créer des tests pour chaque critère d’acceptation, avec des entrées/sorties clairement décrites Pour une API, on peut d’abord produire une spécification complète en OpenAPI ou GraphQL, avec toutes les propriétés et tous les types. On peut ensuite valider les données à l’exécution à partir de cette spécification, et cette spécification elle-même constitue une preuve que l’application fonctionne conformément à ce qui est défini En résumé, il est important d’obtenir, via OpenAPI/GraphQL, les tests et les types, une preuve que le système se comporte réellement comme prévu Si la spécification elle-même est bien conçue dès le départ, on peut ensuite faire évoluer librement l’implémentation du code tout en prouvant sa correction à partir de la spécification La spécification est plus importante que le code lui-même

  • Les cinq propriétés mentionnées dans l’article peuvent être exprimées dans un bon système de types. De cette manière, une grande partie de la spécification devient du code, et le compilateur garantit la correction. L’avenir de la programmation devrait aller dans le sens où cette approche devient la norme Les systèmes de types d’OpenAPI et de GraphQL sont bien trop pauvres ; il leur faudrait sans doute encore 50 ans d’évolution pour atteindre cet avenir

• J’ai étudié les bases de l’informatique théorique à l’université, et je partage l’idée générale de cet article. En pratique, ce n’est pas facile Au-delà des préconditions et postconditions, des techniques de preuve en informatique comme les invariants de boucle (loop invariant) et l’induction structurelle (structural induction) sont extrêmement puissantes Je recommande les liens loop invariant, structural induction, ainsi que les notes de cours CSC236H de l’UofT (notes de cours)

  • Ces notes de cours CSC236 sont excellentes, et le professeur David Liu est vraiment très bien aussi présentation du professeur

  • Tiens, on parle de l’UofT ! Ça fait plaisir

• L’idée de « faire soi-même de petites preuves mentales à propos de son code » est un principe si important qu’il devrait presque aller de soi. Il faut toujours garder à l’esprit de petites propositions sur ce que fait chaque partie du code

  • L’idée est facile à appliquer dans un projet greenfield, quand on vient d’écrire soi-même tout le code, mais elle semble beaucoup plus difficile dans une vraie base de code, où plusieurs développeurs touchent à diverses fonctions ou à un état global

    • Un très bon développeur sait justement faire évoluer progressivement un système dans cette direction. Le code du monde réel est désordonné, mais il est important de réduire peu à peu les failles dans les invariants et de donner à ceux qui viendront ensuite une structure de code qui les aide à en être conscients et à les préserver. La documentation aide, mais d’après mon expérience, la structure du code elle-même joue un rôle encore plus grand

    • C’est précisément pour cela que l’état global est si dangereux. Pour prouver la correction du code, il faut alors connaître l’ensemble du programme. Si on transforme les variables globales en valeurs immuables, qu’on les passe en arguments de fonction, ou qu’on les encapsule dans une classe wrapper qui gère l’état, alors il suffit de comprendre clairement les appelants de cette fonction. Si on ajoute davantage de contraintes à l’intérieur des fonctions, via des assertions par exemple, la difficulté de la preuve diminue nettement. Beaucoup de programmeurs prennent déjà ce genre de décisions, simplement de manière instinctive plutôt qu’en pensant explicitement à la preuve

    • On peut comparer un code dont l’état global est géré par plusieurs développeurs à un patient atteint d’un « cancer métastasé ». Le traitement est bien plus difficile, et selon la chance et les conditions extérieures, il est parfois possible de le sauver

    • Comme le dit l’article, ce type de code a beaucoup plus de chances de produire des bugs, ainsi que des bugs supplémentaires au fil de la maintenance. Cela montre qu’il est bien plus juste d’écrire dès le départ dans une structure qu’on peut raisonner et prouver

    • Ce texte me rappelle que je remets sans cesse en question ma manière de coder, en essayant de la redéfinir dans une meilleure direction. Je me demande si des développeurs comme John Carmack ont aussi, avec le temps, le sentiment que leur ancien code était insuffisant, et s’ils développent une intuition de ce que signifie faire les choses « mieux »

• L’idée qu’un code doit pouvoir être prouvé remonte à la résolution du problème d’exclusion mutuelle par Dekker en 1959. Une anecdote intéressante à ce sujet est racontée dans le texte EWD1303 de Dijkstra (lien original). On peut voir les travaux ultérieurs de Dijkstra comme un prolongement de cette intuition

• Écrire une preuve correcte est vraiment difficile. La vérification de programmes ne l’est pas moins. À mon avis, chercher à faire des preuves à la main n’est pas efficace. Si on écrit un code idiomatique pour le langage et la base de code concernés, on a rarement besoin de se soucier des invariants ou des pré/postconditions. L’accent mis par R. Pike et B. W. Kernighan sur la « simplicité, la clarté et la généralité » dans The Practice of Programming a un effet énorme en pratique. C’est un peu lié mais légèrement différent : en faisant de la programmation compétitive, on apprend clairement qu’il faut maîtriser des techniques garantissant la correction du code pour passer au niveau suivant

  • Je ne suis pas d’accord avec ça. Je pense que l’auteur ne parle pas d’une preuve formelle complète, mais du fait de toujours réfléchir aux propriétés logiques garanties par son code, par exemple les invariants. C’est le meilleur moyen de comprendre le code et de dissiper la peur que son contenu peut inspirer

  • J’ai plutôt l’impression qu’on inverse ici cause et conséquence. Si on aborde le problème avec prudence et réflexion, le code qui en résulte devient naturellement clair et propre. Il faut que la logique soit claire pour que la conception du code le soit aussi. En revanche, croire qu’un code joliment écrit entraînera par lui-même la correction est absurde. Bien sûr, plus le code est propre, moins il y aura de bugs lors d’une revue de code, par exemple. Mais il faut garder à l’esprit que la forme suit la fonction

  • Le concept le plus fondamental d’une preuve, c’est « la raison pour laquelle c’est correct ». Ce n’est pas seulement un moyen d’éviter de petites erreurs, c’est un processus pour vérifier que la direction prise est fondamentalement la bonne

  • Pour assurer la correction du code, il n’existe aucun substitut au fait d’écrire le code correctement. Même si c’est difficile, il faut de toute façon le faire correctement

  • Si on renverse complètement le premier paragraphe, on peut dire qu’avec les bonnes abstractions — c’est-à-dire du code idiomatique adapté au langage et à la base de code — la vérification de programme devient plus facile. Avec des abstractions appropriées, il n’est plus nécessaire de réfléchir aux invariants de boucle, etc., et la preuve découle directement de la correction du code

• La mutabilité et l’immuabilité sont elles aussi des propriétés importantes. Si on garde l’état aussi immuable que possible, on réduit la complexité non seulement en multithreading, mais aussi dans le raisonnement sur l’état du programme

  • L’article original mentionne déjà ce point

• Dans les années 1980, quand j’étais étudiant de premier cycle à Carnegie Mellon, on nous enseignait clairement ce principe. Cela m’a énormément aidé dans la suite de ma vie. Je me souviens en particulier du moment où j’ai appris l’équivalence entre récursion et induction : à partir de là, j’ai pu aborder les algorithmes récursifs proprement, au lieu de « tenter des choses au hasard jusqu’à ce que ça marche »

  • J’ai suivi ce cours récemment, et en étudiant la programmation fonctionnelle, j’ai eu une prise de conscience encore plus forte