Méthodes formelles : simplement une bonne pratique d’ingénierie ? (2024)

 (brooker.co.za)
1 points par GN⁺ 2025-01-12 | 1 commentaires | Partager sur WhatsApp
  • Dans les systèmes bas niveau de grande taille, distribués et critiques, les méthodes formelles doivent être vues non comme une étape supplémentaire uniquement dédiée à la correction, mais comme une pratique d’ingénierie qui réduit le temps et les coûts
  • En logiciel, conception et implémentation se mélangent facilement, si bien qu’une modification tardive de la conception entraîne directement du réusinage de l’implémentation et des coûts liés aux changements d’API
  • Examiner concrètement le comportement et les interfaces avant l’implémentation permet de réduire la densité de bugs et les problèmes après la mise en production, et d’aboutir plus vite à une conception correcte
  • Dans les domaines où les besoins utilisateurs évoluent rapidement ou sont difficiles à formaliser, comme l’UI, la documentation ou la logique tarifaire, l’utilité d’une conception formelle exhaustive en amont peut être moindre
  • Des outils comme TLA+ et P peuvent aussi être utilisés à l’étape de conception pour examiner les optimisations et les contraintes, et ainsi réduire les compromis entre correction et performance

Les méthodes formelles comme bonne pratique d’ingénierie

  • Les méthodes formelles constituent une part importante des bonnes pratiques d’ingénierie logicielle
  • Elles ont une valeur particulière pour les ingénieurs qui travaillent sur des systèmes de grande taille, des systèmes distribués et des systèmes bas niveau critiques
  • Le raisonnement part de l’idée que l’ingénierie consiste en fin de compte à optimiser le temps et les coûts
    • Les performances, la scalabilité, la durabilité et l’efficacité entrent aussi en ligne de compte
  • Les méthodes formelles ne sont ni bon marché ni faciles, et ne s’accordent pas non plus avec toutes les façons de développer, mais l’intuition selon laquelle elles n’ajoutent que du coût n’est pas toujours juste

Deux voies pour réduire les coûts

  • La première est la réduction du réusinage
    • Contrairement à d’autres disciplines de l’ingénierie, en logiciel il est facile que la conception et la construction aient lieu en même temps
    • On peut commencer à implémenter même si la conception n’est pas encore suffisamment avancée
    • Cette malléabilité est une force du logiciel, mais elle peut aussi transformer les itérations de conception en itérations d’implémentation et faire grimper les coûts
  • La seconde est la maîtrise du coût du changement
    • Dès qu’une API ou un système a des clients, le changement devient bien plus coûteux et difficile
    • Selon la loi de Hyrum, dès lors qu’une API a un nombre suffisant d’utilisateurs, quelqu’un finit par dépendre de tout comportement observable, indépendamment du contrat officiel
  • Isoler le comportement d’un système derrière une API est une idée importante de l’ingénierie logicielle, mais cela laisse subsister la limite selon laquelle les utilisateurs peuvent aussi dépendre de détails d’implémentation
  • Même s’il est possible de réimplémenter complètement le système derrière une API, l’abstraction ne supprime pas en elle-même le coût du changement
  • Le travail de conception formelle peut réduire le coût du réusinage et permettre de traiter plus tôt les modifications d’interface, ce qui améliore la vitesse et l’efficacité de construction logicielle

Les systèmes auxquels la conception formelle convient bien

  • Elle ne s’applique pas de la même manière à tous les logiciels
  • Dans les logiciels où les besoins utilisateurs évoluent vite ou sont difficiles à formaliser, la valeur de la conception en amont peut être plus faible
    • Cela inclut l’UI, les sites web ou l’implémentation de logiques tarifaires
    • Dans ces domaines, le réusinage continu peut rendre élevé le coût d’une conception préalable
  • L’idée de base de l’agile est de mener en parallèle l’implémentation et la collecte des besoins afin de réduire le délai jusqu’à la mise en production
    • Cela permet d’achever l’implémentation même lorsque la collecte des besoins se poursuit
    • Dans de nombreux cas, ce mode de développement parallèle est optimal, ou constitue la condition indispensable pour pouvoir avancer
  • À l’inverse, pour une grande partie des systèmes de grande taille, distribués et bas niveau, les exigences sont bien comprises
    • Il existe au minimum une part suffisamment importante d’exigences statiques
    • Dans ce cas, une conception formelle en amont peut réduire de manière significative le réusinage à l’étape d’implémentation ainsi que la densité de bugs et les corrections après la mise en production
  • Plus les exigences se rapprochent de lois physiques, plus la valeur de la conception et de la conception formelle augmente ; plus elles se rapprochent d’opinions d’utilisateurs, plus cette valeur diminue

Les limites de la documentation et de la formalisation des exigences

  • Rédiger clairement les exigences utilisateurs, de façon formelle ou informelle, a une très grande valeur
  • Si les exigences ne sont pas écrites, du temps peut être perdu et des frictions peuvent apparaître parce que les personnes avancent dans des directions différentes
  • Formaliser toutes les exigences humaines peut être difficile ou non économique
    • Exigences esthétiques d’UI
    • Lisibilité de la documentation
    • Cohérence des noms d’API
  • Les divergences d’opinion sur l’approche formelle viennent aussi de conceptions différentes de ce qu’est une approche formelle et de la manière dont elle crée de la valeur
  • Des approches comme UML, qui transposent le code dans d’immenses schémas, peuvent perdre beaucoup de leur valeur si elles ne traitent pas directement les questions difficiles
    • Même un travail utile peut devenir vain s’il est mené avec une mauvaise méthode ou de mauvais outils

Méthodes et outils formels utiles sur le terrain

  • Les méthodes formelles et le raisonnement automatique couvrent un domaine large, avec des outils variés
  • Dans l’univers des grands systèmes cloud, l’ensemble d’outils qui s’est révélé utile comprend notamment :
    • des langages de spécification comme P, TLA+ et Alloy, ainsi que les model checkers associés
    • des outils de simulation déterministe comme turmoil
      • utilisés avec le fuzzing pour explorer systématiquement l’espace d’états par le test
    • des langages de programmation orientés vérification comme Dafny et des vérificateurs de code comme Kani
    • des techniques de simulation numérique
    • des méthodes proches du formel consistant à dessiner sur tableau blanc ou dans des documents de conception des tables de décision, des tables de vérité et des machines à états explicites
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 constitue un bon point de départ pour examiner les méthodes formelles légères
  • La vérification de l’implémentation n’est pas l’unique objectif
    • Des outils comme TLA+ et P ont aussi une grande valeur pour examiner la conception plus rapidement et plus concrètement avant l’implémentation

Créer plus vite des logiciels plus rapides

  • Lors de la rédaction en 2015 de How Amazon Web Services Uses Formal Methods, l’accent portait surtout sur la correction
    • vérifier les propriétés de sûreté et de vivacité de la conception
    • parvenir plus vite à une conception correcte
  • Dans le cas d’une équipe qui utilisait TLA+ pour un système interne de gestion des verrous, le point important était qu’elle avait « vérifié des optimisations agressives »
  • Des outils comme TLA+ peuvent non seulement permettre de créer plus vite un système, mais aussi de créer un système plus rapide
    • en explorant rapidement les optimisations possibles
    • en identifiant les contraintes vraiment importantes
    • en vérifiant que l’optimisation proposée est correcte
  • Dans bien des cas, les méthodes formelles réduisent les compromis difficiles entre correction et performance dans lesquels les systèmes tombent facilement

La valeur des outils utilisés à l’étape de conception

  • Utiliser à l’étape de conception des outils qui aident à réfléchir à l’architecture d’un système peut fortement accélérer le développement logiciel
  • Cela permet de réduire les risques et de construire dès le départ des systèmes mieux optimisés
  • Pour les ingénieurs qui construisent des systèmes complexes à grande échelle, les méthodes formelles font partie des bonnes pratiques d’ingénierie

À lire aussi

1 commentaires

 
GN⁺ 2025-01-12
Commentaires sur Hacker News

  • La vérification formelle des logiciels dépend fortement, comme l’article le reconnaît, du type de logiciel et du processus de développement.
    Pour utiliser la vérification formelle, il faut disposer d’exigences formelles sur le comportement du logiciel, ce qui ne correspond pas à la plupart des projets ni des philosophies de conception. Si le développement et la conception avancent ensemble alors qu’on ne sait même pas précisément ce que l’on veut, les méthodes formelles sont difficiles à appliquer. En revanche, les domaines qui reposent sur des spécifications préalables, comme les petits systèmes critiques pour la sécurité, peuvent en tirer un grand bénéfice ; les logiciels aérospatiaux en sont l’exemple typique.

    • Je n’ai pas eu l’impression que ce soit une niche à ce point. Le coût dont parlent les gens a beaucoup baissé au cours des dernières décennies, et j’ai déjà vu des outils comme TLA+ ou Alloy être enseignés à des développeurs en moins d’une semaine.
      Aujourd’hui, ce n’est plus une compétence qui exige un doctorat ou des années de recherche, et il en va de même pour l’écriture de spécifications de haut niveau de base. Avec un model checker, on apprend quelque chose sur le système que l’on modélise, et c’est utile même si l’on ne s’en sert que pour la documentation ou la formation. La force fondamentale des méthodes formelles est qu’elles obligent à pousser le raisonnement jusqu’au bout. Beaucoup de développeurs pensent pouvoir implémenter des algorithmes concurrents avec leur seule tête, un vérificateur de types et quelques tests unitaires, mais après avoir lancé un model checker et découvert des erreurs dans leur conception et leurs hypothèses, on devient forcément plus humble. Il existe beaucoup de systèmes distribués plus petits qu’on ne l’imagine, et l’espace d’états est souvent bien plus grand que prévu avant de le formaliser.
    • Ce n’est pas tout ou rien. Je travaille sur un backend très orienté produit qui n’est pas entièrement spécifié, mais certaines parties l’ont été formellement.
      Par exemple, nous avons ajouté des tests basés sur les propriétés à une machine à états très délicate, afin de vérifier que, quels que soient les appels aux endpoints avec des entrées étranges, la machine à états interne n’effectue pas de transition invalide. Le code autour n’avait pas de spécification formelle, mais la machine à états, elle, en avait une ; c’est ce qui l’a rendu possible, et nous avons trouvé des bugs subtils que des tests unitaires classiques n’auraient jamais détectés.
    • « Formel » signifie « écrit dans un langage interprétable par un ordinateur », et c’est précisément ce que font les programmeurs. Écrire du code, c’est écrire une spécification formelle du comportement d’un programme ; par définition, tout logiciel doit le faire.
      Cela dit, pour bénéficier des méthodes formelles, il faut comparer le comportement du programme à autre chose qu’au programme lui-même, et cet autre élément doit lui aussi être écrit dans un langage formel. Il faut comprendre précisément le comportement souhaité, mais il n’est pas nécessaire de couvrir tout le comportement du logiciel. Les tests unitaires automatisés sont eux aussi des spécifications formelles, et les exécuter est une méthode de vérification formelle. Ce ne sont que des spécifications et une vérification plus faibles que ce que l’on appelle généralement méthodes formelles ; il n’y a pas de différence qualitative nette, ni conceptuelle ni pratique. Si un logiciel se prête aux tests, il y a de fortes chances que des méthodes de spécification formelle plus riches puissent également s’y appliquer, et l’on apprend leur rapport coût-efficacité par essais et erreurs, comme on apprend à tester.
    • Qu’on le veuille ou non, des exigences finissent toujours par apparaître. La seule différence est de savoir si on les découvre pendant la phase d’ingénierie des exigences, en les validant dans un simple document texte et en résolvant les conflits, si on les découvre après les avoir mal implémentées en codant, ou si c’est le client qui les découvre lors d’une « sprint review ».
      Au bout du compte, la question est de savoir combien d’argent et de temps supplémentaires on veut dépenser pour pouvoir appeler cela de l’« agile ». Paradoxalement, la phase traditionnelle de recueil des exigences est la moins coûteuse des trois approches et celle qui correspond le mieux à l’esprit agile originel, puisqu’elle permet de converger rapidement avec le client au moment où le coût du changement est le plus faible : lorsqu’il suffit de modifier une ligne de texte.
    • Le point clé semble être moins la conception en amont que la possibilité de formalisation. Par exemple, un système d’automatisation des demandes d’indemnisation d’assurance ne peut souvent pas être conçu dès le départ, car le fonctionnement des assureurs n’est pas explicite, mais on peut affiner le système d’automatisation au fil des interactions et des informations obtenues.
      Malgré tout, on peut en tirer le bénéfice de vérifier qu’aucun cas n’a été oublié et qu’il n’existe pas de contradiction dans le système.

  • À propos des méthodes formelles, on voit souvent le raisonnement suivant : « le logiciel est vaste, complexe et difficile à réussir, donc méthodes formelles »
    D’un côté, j’aimerais que ce soit vrai. C’est une façon de travailler que l’on apprend dans le monde académique et dans laquelle je suis à l’aise, donc j’y gagnerais personnellement ; et, en pratique, quand un logiciel échoue réellement à cause de sa complexité, il est frustrant de devoir errer à la recherche de la cause. Mais on montre rarement de manière convaincante comment les méthodes formelles résolvent ce problème. Cet article est meilleur en ce qu’il souligne que la majeure partie du « design » moderne est une perte de temps, mais il n’explique pas suffisamment pourquoi TLA serait meilleur qu’UML. On a presque l’impression qu’il suggère qu’après avoir investi des mois, voire des années, dans TLA, on atteint une forme d’illumination et l’on comprend son utilité d’une manière impossible à expliquer à ceux qui ne l’ont pas vécue. Le calcul différentiel ou les statistiques bayésiennes ont aussi un peu ce côté-là, donc ce n’est pas impossible ; mais on finit par revenir au jugement de chef de projet : « si c’était vraiment aussi utile, davantage de gens l’utiliseraient et ses avantages seraient évidents d’eux-mêmes ». Si cela existe depuis longtemps sans s’être largement imposé, il y a probablement une raison

    • À mon avis, si UML est inutile, c’est parce qu’un même diagramme peut être compris différemment selon les personnes et que, bien qu’il puisse être très complexe, il n’est pas vérifiable, ce qui permet de produire des diagrammes UML contradictoires ou absurdes
      Quand on rencontre un problème difficile à raisonner, on finit par utiliser une certaine « méthode ». Pour un protocole de communication, il est pertinent de le décrire comme une machine à états, et TLA s’insère mieux dans ce créneau. Ces derniers temps, il n’y a pas eu beaucoup de problèmes qui justifient un tel effort, mais quand ils apparaissent, la valeur est immense. Il en va de même pour les langages spécifiques à un domaine : pour éviter de nombreux problèmes, il vaut bien mieux utiliser un framework de parsing que d’écrire soi-même un parseur. Aujourd’hui, la majeure partie du retravail vient des changements d’exigences et du fait que les clients disent « ce n’est pas ça » sans savoir ce qu’ils veulent réellement. Il y a aussi le fait que les demandeurs ne réfléchissent pas assez aux implications de leurs exigences, mais le problème principal est plutôt que les connaissances nécessaires pour prendre de bonnes décisions ne sont pas suffisamment réunies au même endroit
    • Si les méthodes formelles ne sont pas largement utilisées, c’est, à mon avis, parce qu’il n’existe pas tant de domaines métier où il vaut vraiment la peine de consacrer beaucoup de temps et d’argent pour faire passer l’exactitude de la logique métier de 98 % à 99,99 %
      Les méthodes formelles représentent clairement un gros investissement. Cela dit, même si elles ne se sont pas imposées de manière générale, une partie de leurs idées a été intégrée aux systèmes de types modernes
    • Je n’ai été exposé à la vérification formelle que dans le contexte de cours de hardware ; c’est proche de la programmation, mais le rapport coût/bénéfice est complètement différent. Une puce physique ne peut pas être facilement corrigée après fabrication, et les types de conception sont très différents
      L’impression que j’en ai gardée est que la rigueur d’un vérificateur formel impose des limites à la complexité de la conception, ne serait-ce que parce qu’il doit terminer dans un temps et une mémoire raisonnables. Peut-être que le vrai gain d’exiger une vérification formelle est de corriger le problème selon lequel « le logiciel est vaste, complexe et difficile à réussir » en rendant simplement pénible la gestion de gros programmes complexes
    • Pour faire bouillir cette grenouille lentement, il ne faut pas tant enseigner TLA que lui voler sa sagesse. Les systèmes de types ont beaucoup emprunté à Hindley-Milner, qui est en soi une forme de preuve partielle formelle
      J’aimerais voir des descendants du test basé sur les propriétés qui utilisent des techniques SAT ou TLA pour réduire rapidement et de façon reproductible l’espace d’entrée. À partir du parsing et de la couverture de code, on devrait pouvoir déduire que passer 12 à une fonction ne peut pas emprunter une branche différente de 11, mais que des valeurs comme -1 ou 2^17 < n < 2^32 pourraient, elles, se comporter différemment
    • L’argument « si c’était vraiment utile, davantage de gens l’utiliseraient » n’est bon dans aucun domaine, et il est deux fois plus mauvais dans le développement logiciel
      Aujourd’hui encore, la plupart des projets logiciels échouent. Ce n’est pas une « défaillance de marché », c’est plutôt tout simplement un « échec à construire »

  • Il existe grosso modo deux branches dans les méthodes formelles : les méthodes extrinsèques, séparées du code lui-même et qui infèrent généralement les spécifications du code, et les méthodes intrinsèques, intégrées au code et qui raisonnent plus directement sur celui-ci
    Historiquement, les méthodes intrinsèques comme les systèmes de types raisonnaient sur le code au niveau des fonctions, tandis que les méthodes extrinsèques comme les model checkers décidables tels que Spin/P manipulaient des modèles de code décrits dans des formalismes comme les automates. Je considère que nous sommes aujourd’hui dans un âge d’or de la recherche sur les méthodes formelles ; par rapport aux méthodes intrinsèques poussées par les progrès des systèmes de types et des projets comme Verus, les méthodes extrinsèques semblent de moins en moins privilégiées. https://github.com/verus-lang/verus

    • Les outils comme TLA+ fonctionnent bien parce qu’ils ciblent un langage de spécification très petit
      J’ai vu la question de savoir comment cela fonctionnerait avec un langage à grande empreinte comme Rust, mais je n’ai pas encore vu de bonne réponse. J’aimerais en lire davantage
    • Si le projet Verus lié demande lui aussi d’écrire directement des spécifications d’exactitude, je ne vois pas bien pourquoi cette distinction est significative
      J’avais compris que les méthodes intrinsèques étaient préférées parce qu’elles évitaient d’écrire et de maintenir des spécifications séparées, mais en pratique ce n’est pas le cas

  • Le passage sur les méthodes formelles légères est pertinent. Maintenir un ensemble de stratégies proptest à côté d’une base de code ne représente pas un investissement beaucoup plus important que d’écrire des tests unitaires à la main, mais offre une bien meilleure visibilité grâce à une large couverture et à de petits cas d’échec compréhensibles
    Surtout, cette approche s’intègre bien aux pratiques habituelles de développement logiciel. https://crates.io/crates/proptest

    • De nos jours, on génère beaucoup de tests unitaires avec des LLM. Ils s’en sortent plutôt bien, et on peut leur demander d’être un peu plus rigoureux, de tester les cas limites qui viennent à l’esprit ou de gérer certaines conditions particulières
      Je sais dans une certaine mesure comment écrire de bons tests et l’effort que cela demande, mais un LLM peut produire de meilleurs tests que moi beaucoup plus rapidement. Face à une tâche répétitive et ennuyeuse, il est même moins susceptible que moi de bâcler le travail quand ma patience diminue. Un ingénieur logiciel devrait avoir le réflexe d’automatiser ce qui lui semble répétitif, et aujourd’hui la documentation aussi est générée, ce qui pousse à en faire plus souvent et plus tôt. Les LLM pourraient provoquer une petite révolution dans l’adoption de la vérification formelle. Générer de bonnes spécifications est fastidieux, mais avec suffisamment de contexte — code fonctionnel, documentation, indices — cela peut être une tâche relativement facile pour un LLM. Si l’on peut les faire générer puis les relire, plutôt que de les écrire entièrement soi-même, on est bien plus enclin à le faire. Utiliser Rust est aussi un signal que l’on accorde de l’importance à l’exactitude, et son compilateur est probablement l’outil qui se rapproche le plus d’une preuve, sans méthodes formelles, que le système est probablement correct. C’est probablement beaucoup plus facile que d’ajouter des méthodes formelles à un langage dépourvu de compilateur ou de types explicites
    • proptest ou qcheck ne sont pas des méthodes formelles, mais des tests aléatoires

  • La vérification formelle de logiciels reste trop difficile à utiliser pour que cela en vaille la peine, sauf dans les cas extrêmes. À l’inverse, la vérification formelle du matériel est à un niveau où il n’y a aucune raison de s’en passer
    J’essaie sans cesse d’apprendre, mais pour la plupart des systèmes il faut être un expert du niveau de « quelqu’un qui a écrit le compilateur lui-même ». Par exemple, j’ai essayé de prouver un encodeur/décodeur varint : ça a marché pour 1 ou 2 octets, mais pas au-delà. Quand j’ai demandé de l’aide, il s’est avéré que c’était dû à des détails internes impossibles à deviner, du genre le compilateur ne déroule la boucle que 5 fois en interne. J’apprends Lean récemment, et j’aime bien, mais je tombe sur des docs du type : « Definitional equality includes η-equivalence… ». Je ne cherche pas à dénigrer Lean ; au contraire, sa documentation me semble plutôt meilleure que celle des alternatives

    • Je me demande si vous avez essayé FizzBee.io. Il utilise une syntaxe proche de Python et les exemples valent le coup d’œil : https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      Les méthodes formelles n’ont pas forcément besoin d’être compliquées. Le problème, c’est que la plupart d’entre elles semblent conçues comme des exercices académiques destinés à illustrer un sujet précis qui intéressait un professeur. TLA+ aussi a plutôt été conçu dans une optique de rédaction d’articles
    • Ça peut faire peur, mais ces concepts sont en réalité tous très simples, et il y a de fortes chances que vous les connaissiez déjà

  • Parmi les méthodes formelles légères, une que j’aime bien, même si elle n’est pas très connue, est la vérification de traces à l’aide de la logique temporelle linéaire : https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    En gros, il suffit de journaliser les événements, et dans une architecture événementielle on peut presque l’obtenir gratuitement. Ensuite, on exécute des prédicats comme Always(Locked, Implies(Eventually(Unlocked))) sur la trace d’exécution. On peut aussi l’appliquer à des traces passées, et le combiner avec des stress tests ou du fuzzing pour explorer l’espace d’états. C’est simple, puissant, largement applicable, et il suffit d’avoir des prédicats, sans modèle

    • Petite distinction, mais cela se rapproche davantage du test, puisque l’on vérifie une formule seulement sur un sous-ensemble des traces du système
      Les méthodes formelles impliquent une justification exhaustive du comportement du système. Dans TLA ou des systèmes similaires, même s’il s’agit d’une machine à états et non du système réel, le résultat est une preuve que des propriétés LTL/CTL/TLA sont valables pour tous les comportements du système, c’est-à-dire pour toutes les traces ou tous les arbres de traces

  • Une discussion précédente a eu lieu en juin 2024 : https://news.ycombinator.com/item?id=40753989

  • C’est beaucoup trop lent. Un plan devient vite fossilisé, et n’importe quel document peut être utilisé comme preuve à charge devant le tribunal agile

    • Pour le dire de façon polémique, si le « vrai agile » était découvert, les méthodes formelles en seraient l’exact opposé. Car tout ce qui est prouvable et reproductible relève du blasphème pour les vrais croyants

  • La plupart des textes que j’ai lus sur les méthodes formelles donnent l’impression de servir à générer des prospects pour des consultants
    En soi, ce n’est pas grave, mais c’est désagréable quand quelqu’un se comporte comme s’il avait atteint l’illumination grâce aux méthodes formelles, en promettant de corriger les mauvaises habitudes de programmation — voire des habitudes dangereuses de manière irresponsable — de mes employés ou collègues si j’achète son package de formation ou si je l’embauche. Quand les méthodes formelles généreront réellement du code de haute qualité incapable de s’écarter de la spécification, on en reparlera

    • Et https://en.wikipedia.org/wiki/SPARK_(programming_language) ?
    • « Générer du code de haute qualité incapable de s’écarter de la spécification » serait utile, mais il y a un problème fondamental : le code est trop concret
      Dans une spécification formelle, on ne va généralement pas jusqu’à ce niveau de détail ; on spécifie le comportement général du système. Il arrive donc souvent qu’une même spécification corresponde à de nombreux programmes subtilement différents. C’est aussi pour cette raison que le code ne suffit pas comme documentation : on ne peut pas savoir ce qui relève d’un choix intentionnel et ce qui relève d’un accident. Le code est trop concret pour décrire des exigences de haut niveau. À l’inverse, vérifier un programme par rapport à une spécification a plus de chances d’être réalisable

  • Certains défenseurs actuels des méthodes formelles considèrent ceux qui ne les utilisent pas comme « paresseux » ou « idiots », et cherchent à affirmer leur supériorité au motif qu’ils « font ce qu’il faut » ou qu’ils « maîtrisent un langage complexe »
    Bien sûr, ce n’est pas le cas de tous, et je connais aussi des gens très bien, mais certains ressemblent en fait plutôt à des gens qui n’ont qu’une seule corde à leur arc. Quand on leur demande quels autres systèmes de méthodes formelles ils ont appris ou essayés ces dernières années, ils répondent qu’ils sont « trop occupés » pour apprendre quelque chose de nouveau. Parmi les méthodes formelles récentes plus faciles à utiliser, il y a FizzBee, qui utilise un dialecte de Python et se lit comme du pseudocode, Quint, avec une syntaxe plus simple, et P, dont la syntaxe est familière aux utilisateurs de C#. L’auteur de cet article a aussi écrit que les méthodes formelles ne résolvaient que la moitié de son problème : https://brooker.co.za/blog/2022/06/02/formal.html
    Mais le problème mentionné là-bas est déjà résolu par PRISM, qui n’est même pas nouveau. C’est simplement que Brooker ne cherche pas autour de lui, ou ne veut pas apprendre