Bon article. Pour avoir déjà fait de la vérification de programmes, Rust me semble être le langage moderne le plus utile pour appliquer des méthodes formelles
Les règles de Rust éliminent beaucoup de cas difficiles à formaliser. Le gros problème restant est l’analyse des interblocages du point de vue des threads et du point de vue Rc/emprunts, les deux étant dans une certaine mesure équivalents. S’il existait une analyse statique des interblocages en Rust, des pointeurs de déréférencement sûrs deviendraient probablement possibles ; et si l’on pouvait prouver que tous les appels borrow/upgrade ne peuvent pas échouer, on pourrait supprimer la plupart des comptages de références. On obtiendrait alors gratuitement la mutabilité interne quand c’est possible
Le gros problème des prouveurs de théorèmes, c’est qu’ils sont conçus par des gens qui aiment prouver des théorèmes : ils tombent dans le formalisme et leur sens de l’UI diverge de celui des programmeurs. La plupart des obligations de preuve peuvent être traitées par un solveur SAT, mais les problèmes difficiles nécessitent des outils plus lourds. Coq est trop manuel, et l’auteur juge ACL2 trop fonctionnel. Le machine learning peut aider à orienter un prouveur de théorèmes. Il est difficile de lui confier la preuve elle-même, mais inférer des plans de preuve dans du code où le flux de contrôle et l’usage des données se ressemblent globalement semble possible
F* est proche du langage mythique qui prouve automatiquement. Il utilise un solveur SMT, plus puissant que SAT, et permet aussi des preuves manuelles quand la résolution automatique échoue
Les routines cryptographiques de Firefox et Wireguard ne sont pas écrites en Rust, mais en F*, plus précisément en Low*, un DSL bas niveau intégré à F*, et elles sont entièrement vérifiées https://project-everest.github.io/ https://mitls.org/
Je suis d’accord, mais je pense que Lean, grâce à ses riches capacités de métaprogrammation, fait de grands progrès en matière d’expérience utilisateur pour la vérification interactive de preuves de théorèmes
Le problème, quand on applique ce type d’outil à la vérification d’un langage externe comme Rust, c’est que les preuves ne sont pas écrites dans le langage cible, ce qui oblige les développeurs à apprendre deux langages. À partir de mon expérience sur Creusot, de mon travail sur Verus et Aeneas, et de mon expérience au laboratoire Why3, j’ai réfléchi à ce à quoi pourrait ressembler un « Rust pensé pour la vérification ». Si l’on concevait un tel langage dès le départ, sa facilité de vérification pourrait progresser par paliers par rapport à Rust, avec un impact particulièrement fort sur les parties difficiles des preuves
Je pense que la famille Coq/Agda/Lean finira par l’emporter dans le domaine de la preuve. L’interaction est un assez bon modèle de boucle de rétroaction, et ce sont des systèmes qui existent déjà et fonctionnent réellement
Ce qui me manque le plus dans les fonctionnalités de base, c’est l’équivalent de « lance quickcheck sur ma preuve ». Quand on a du code et qu’on essaie de prouver une propriété qui est fausse, il est facile de s’arracher les cheveux à comprendre pourquoi la preuve ne passe pas. Si, au milieu d’une preuve, on atteint un état absurde, ce serait bien qu’une commande du type « génère un contre-exemple à partir d’ici » en produise un. Les preuves sont très dépendantes du chemin suivi et ne sont généralement pas faciles, mais ces outils semblent tout proches de quelque chose de grand. Le processus consistant à prouver du code doit aussi refléter la possibilité que ce code contienne des bugs
L’idée que le machine learning guide les prouveurs de théorèmes est intéressante. Si le système de machine learning a raison, il mène à une preuve valide et le gain est important ; s’il se trompe, le coût n’est pas très élevé
Le prouveur ne produit pas de preuve incorrecte, il échoue simplement à dériver une preuve valide. Je ne pense pas qu’il existe beaucoup d’applications du machine learning ayant cette propriété
Je ne suis pas spécialiste de la vérification formelle, mais je ne pense pas que les verrous, au sens traditionnel, aident beaucoup. Aucun compilateur ne fournit quelque chose de vraiment utile à propos des verrous ; il faut simplement accepter le risque et vivre avec
En réalité, en Rust, les verrous et le comptage de références sont des structures d’exécution. Arc casse largement le modèle RAII de Rust, au point qu’il a fallu supprimer les scoped threads, dont le destructeur devait s’exécuter avant la fin de la portée. Le comptage global de références pose des problèmes de cycles et de fuites, et redevient un problème global. Il sera difficile de s’en passer complètement, mais je pense qu’il vaut mieux l’enfermer dans des portées de style arena. Les verrous semblent nécessiter des structures de données asymétriques, comme les canaux. En Go, on sépare un canal en émetteur et récepteur, et on peut faire un defer close(ch) dans la goroutine émettrice ; même en cas de panique, son exécution est garantie lorsque le reste du thread se termine. Il n’est pas nécessaire que ce soit des canaux, mais séparer les rôles lecture-écriture/producteur-consommateur rendrait le raisonnement beaucoup plus simple et aiderait aussi l’analyse formelle
J’aime bien le fait que cela parte d’une citation d’un article de Hoare vers 1973 et que cela se poursuive maintenant jusqu’à un deuxième billet. À l’origine, j’avais laissé un long commentaire dans le fil HN du billet de boat, en disant que faire pencher cette citation vers une perspective centrée sur Rust était compréhensible vu le parcours de boat, mais réduisait artificiellement la portée de la critique de Hoare
Grayson a maintenant pris ce fragment étroit comme point de départ pour discuter de quelques domaines et points de conception intéressants de Rust. Je pense toujours que mon commentaire était juste, mais la discussion issue du billet de Grayson a suffi à compenser mes réserves techniques sur le texte qui en était le point de départ
Vers le milieu des années 1990, Hoare lui-même avait déjà remarqué qu’il pouvait y avoir quelque chose de problématique dans les fondements de l’approche centrée sur la solidité des années 1970 : http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Depuis, avec l’apparition de techniques non sound plus avancées que le simple test, je pense que les méthodes non sound ont pris de l’avance sur les méthodes sound
1973, c’était il y a 50 ans, soit toute une vie professionnelle d’expert. Hoare est vraiment passé très près
Il avait identifié le problème et, avec le recul, la solution consistant à imposer par le système de types la mutabilité XOR partagée paraît n’être qu’un petit pas. Si l’on avait compris à l’époque que ce petit pas était la solution, on aurait évité 50 ans d’énormes souffrances
Voici ce que j’avais écrit à l’origine à propos de la citation de l’article de Hoare par boat. Après la première citation de Hoare et une brève introduction, l’auteur dit que « quand Tony Hoare disait que les références sont comme des sauts, il parlait du problème de l’état mutable et aliasé ». withoutboats étant un développeur Rust connu, cette interprétation n’est pas surprenante
Mais la citation elle-même ne me semble pas renforcer ce point de vue. On peut y voir une tentative de prendre le regret plus général exprimé par Hoare sur l’existence sémantique même des références et de l’appliquer au modèle Rust d’état mutable non aliasé afin de contourner le problème. Mais cela revient plutôt à corriger un fragment étroit d’un problème plus vaste, puis à dire que tout le problème a disparu. Les parties omises, en particulier le début de la section « Variables » et l’exemple ALGOL 68, penchent beaucoup plus fortement vers l’idée que Hoare critiquait non pas seulement l’état mutable, mais le concept sémantique même de référence. Je reconnais que Rust tente de dompter une partie du problème, mais je ne pense pas qu’un langage quelconque l’ait « corrigé »
Je ne comprends pas très bien pourquoi ce billet reçoit autant d’éloges. J’ai l’impression qu’il balaie en un paragraphe plusieurs domaines de l’analyse de programmes. J’aime bien Graydon et je respecte son point de vue, mais ce paragraphe est beaucoup trop simplificateur
Dire que les langages avec GC ne se seraient pas vraiment dotés d’un solide support du raisonnement local est un homme de paille. Il y a eu des langages comme Pony, qui mettent des régions dans le système de types tout en utilisant un GC. Il existe aussi tout le domaine de l’analyse de pointeurs et de l’analyse d’échappement, qui infèrent l’unicité et déterminent si deux références peuvent être des alias. Le cœur du typage statique consiste aussi, via les classes et les champs, à diviser le tas en parties qui ne s’aliasent pas mutuellement. On ne parle pas de JavaScript, et il ne faut pas faire comme si Java/C#/Scala et d’innombrables langages avec GC n’avaient aucun raisonnement local sur l’état mutable
Dans le cas général, on ne peut pas faire cela automatiquement de façon complète, et en pratique il faut quelque chose d’assez proche de la logique de séparation. La sémantique du borrow checker de Rust peut aussi être vue comme une forme simplifiée de logique de séparation
Les classes et les champs ne fournissent pas un raisonnement local complet sur l’état mutable. En effet, une classe/un objet A peut finir par dépendre de l’état mutable d’une classe/d’un objet B. L’héritage de classes à la Java ajoute lui-même davantage de complexité à mesure que le programme évolue dans le temps
Graydon ne dit pas que le GC rend impossible un fort raisonnement local. Il dit que, pour une raison ou une autre, la plupart des concepteurs de langages ont fait des choix allant à l’encontre de cet objectif, et cela me paraît manifestement vrai
Il existe bien sûr des contre-exemples, mais si l’on regarde les langages généralistes grand public avec GC comme Java, C# ou Python, c’est exact. On peut interpréter l’idée originelle de l’orienté objet comme proche de l’actor model actuel, avec des structures de données possédées que l’on ne modifie que par passage de messages. Mais les implémentations réelles de l’orienté objet sont loin d’approcher cet objectif. Java n’empêche pas de stocker des références mutables au même objet dans plusieurs objets. Ce billet explique mieux ce point : https://without.boats/blog/references-are-like-jumps/
Petit quiz : qu’affiche ce code ? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Édition : j’ai mal lu une double négation. Même en relisant, cela reste confus pour moi. Cela veut-il dire que Java, contrairement à JavaScript, dispose d’un raisonnement local ?
J’aime généralement les billets de Graydon, mais celui-ci, comme beaucoup de textes sur les méthodes formelles, peut induire en erreur les lecteurs qui ne connaissent pas le domaine. C’est un peu comme dire que la manière de transformer le plomb en or s’est améliorée d’un ordre de grandeur à un seul chiffre, sans préciser qu’il manque encore 29 ordres de grandeur pour que ce soit rentable en pratique
Est-ce que l’absence d’alias facilite beaucoup la vérification formelle ? Oui. Est-ce que cela permet pour autant de vérifier des programmes réels de manière pratique et économiquement efficace ? Pas du tout. Il existe des programmes, des circuits et des composants vérifiés formellement au quotidien, mais ils relèvent plutôt de l’exception, sont relativement très petits et sont conçus d’une manière particulièrement prudente. Les propriétés qui aident au raisonnement local sont importantes, mais elles ne changent pas vraiment la façon de garantir, de manière rigoureuse, la correction des logiciels grand public
Même les programmes écrits dans un langage très éloigné de la complétude de Turing — sans tas, sans pointeurs, sans entiers, avec seulement des variables booléennes, et dont les boucles ne peuvent pas s’exécuter plus de deux fois — ne peuvent pas être vérifiés de façon pratique, car ils se réduisent à TQBF. Pour certaines propriétés, par exemple la sûreté mémoire, c’est possible, mais cela ne suffit pas à ce dont les logiciels ont besoin. Dans les années 1970 à 1990, on espérait que, même si la complexité dans le pire cas était ingérable, les garanties locales et la structure des langages permettraient d’éviter ce pire cas ; depuis, il a été démontré que ce n’était pas le cas. L’espoir que les programmes réellement écrits par les humains soient suffisamment éloignés du pire cas pour permettre de bonnes heuristiques ne semble plus tenir non plus
Il existe une présentation sur le sujet : https://pron.github.io/posts/correctness-and-complexity
Le résultat essentiel est que la plupart des propriétés intéressantes que l’on voudrait vérifier ne se composent pas. Même si l’on prouve la propriété pour chacun des composants P1...Pn, le coût de prouver cette propriété pour P1 ○ ... ○ Pn ne croît pas seulement de façon superpolynomiale en n, mais aussi de façon superpolynomiale par rapport à la taille de chaque composant. Autrement dit, c’est aussi difficile que si l’on n’avait rien découpé, et la correction ne se décompose pas. C’est pourquoi « on peut vérifier pas mal de choses » et « ce qui est vérifiable n’est qu’une goutte d’eau dans l’océan » sont simultanément vrais, et cet écart est souvent absent des discussions sur les méthodes formelles
Cela fait plus de six ans que tu répètes le même raisonnement des centaines de fois sur HN, et malgré les nombreux commentaires reçus entre-temps, presque aucune nuance ne s’y est ajoutée
Ce n’est pas totalement faux, mais ce n’est pas totalement juste non plus. Il est étonnant que, malgré les nombreuses occasions qu’ont eues les personnes intéressées par ce sujet de le montrer au fil de ces centaines de répétitions, ta position n’ait absolument pas évolué. Cette attitude donne l’impression d’une fermeture maladive et finit par faire perdre leur temps à tous ceux qui participent à la discussion
Je pense que se focaliser sur la solidité détourne l’attention de techniques qui, en pratique, ont donné de meilleurs résultats pour atteindre l’objectif de logiciels plus corrects. Il existe des techniques pratiques également étayées par la théorie, et elles surprennent parfois même ceux qui pensaient que la solidité était la seule voie : http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Ce schéma se répète. Même pendant que des méthodes solides connaissent des améliorations importantes, des méthodes non solides réalisent en pratique des progrès bien plus grands vers des logiciels plus corrects. Un exemple très récent est https://antithesis.com. Bien sûr, dans certaines situations, les techniques solides peuvent être plus puissantes et plus pratiques ; c’est donc un sujet complexe
Il est raisonnable d’espérer que l’on pourra vérifier que de petites bibliothèques Rust utilisent correctement unsafe. Rien que cela serait vraiment utile
Je viens aussi de laisser un commentaire connexe sur le billet consacré à F*. À en juger seulement par la syntaxe, je préfère subjectivement F*/F# à Rust, mais pour le logiciel de contrôle de spectacle que je développe, j’ai décidé d’utiliser Ada/SPARK2014
Pour que Rust attire le même type de personnes qu’Ada/SPARK2014, il lui faut une norme officielle publiée, comme les langages existants tels que C, Common Lisp, Prolog, Fortran ou COBOL. Rust commence à y entrer, avec la collaboration d’AdaCore et de Ferrous Systems pour proposer des outils de vérification formelle pour Rust comme pour Ada/SPARK2014, mais il n’existe pas encore de norme publiée, et l’héritage d’Ada et de SPARK2014 est immense
Il est intéressant de voir le comptage de références comme une sorte de GC optimisé à exécution immédiate, qui fonctionne lorsqu’on l’utilise strictement pour des données acycliques ou lorsqu’on peut accepter les fuites dues aux cycles. Python utilise l’approche hybride comptage de références + traçage décrite dans l’article, et j’ai aussi vu des déploiements en production où l’on forçait le collecteur par traçage à ne s’exécuter qu’une fois tous les N requêtes
Perl repose sur du comptage de références pur, mais dispose de références faibles, ce qui permet de rendre les données acycliques du point de vue du comptage de références, au prix de devoir faire attention aux parties d’une structure cyclique dont on conserve les références. Koka utilise en théorie le comptage de références, mais essaie en pratique d’en déplacer autant que possible à la compilation ; si, dans y = x + 1, il est garanti que x n’a qu’une seule référence et ne sera plus utilisé ensuite, il peut réutiliser le même stockage pour y et effectuer une modification en place
Nim propose ORC, qui ajoute au comptage automatique de références une implémentation de l’algorithme Recycler de Bacon+Rajan. Cet algorithme est conçu pour ne collecter que les cycles dans les systèmes fondés sur le comptage de références, et il est assez rapide. Pour revenir à Rust, on trouve ici une implémentation stop-the-world de Recycler : https://github.com/fitzgen/bacon-rajan-cc et elle est publiée sous forme de crate bacon-rajan-ccc dans ce fork : https://github.com/mbartlett21/bacon-rajan-cc La section Alternative du README contient des liens vers d’autres expérimentations dans le même domaine. Si l’article Recycler est difficile à trouver, j’en ai rassemblé des copies sous https://trout.me.uk/gc/, et si vous avez des goûts similaires, les articles sous https://trout.me.uk/lisp/ pourraient aussi vous plaire
Firefox utilise lui aussi le comptage de références avec un collecteur de cycles fondé sur la suppression à l’essai pour gérer les cycles entre objets DOM C++ et JS. En fait, Graydon s’est chargé de l’implémentation initiale
La vérification formelle des programmes me rend impatient. La preuve qu’un programme implémente correctement une spécification est intéressante en théorie, mais peu utile en pratique
Écrire une spécification correcte est aussi difficile que programmer correctement : le problème difficile n’est donc pas résolu, seulement déplacé. Les méthodes formelles ont des usages pratiques, mais on les rencontre rarement
C’est vrai pour une spécification complète, mais ce n’est pas vraiment l’objectif. En général, ce qu’on veut prouver, ce sont quelques propriétés clés. Par exemple, que cette fonction termine toujours, ou que cette autre renvoie toujours un tableau trié
Une fois qu’on peut faire cela, on peut l’imposer comme précondition. Par exemple, devoir montrer qu’un tableau est déjà trié avant de le passer à une fonction
Le texte a été écrit le 15 mai 2024, jour du 9e anniversaire de Rust 1.0
J’ai lu l’article de Boats mis en lien, et il était excellent. J’ai été surpris de voir que la citation de Hoare, vieille de 50 ans, reste pertinente et qu’elle est aussi bien formulée
J’aimerais pouvoir utiliser quelque chose de plus simple, comme des type guards à la compilation. Quand les trait bounds prolifèrent, les programmes au niveau des types deviennent difficiles à lire
Par exemple Where <<::Output as G>::Output as H>::Output: HList + Z ou type Output = <<::Output as G>::Output as H>::Output;. On y ajoute Cons>>>, puis on se rend compte que des nombres comme U8 de TypeNum sont eux-mêmes des imbrications de Cons>>. On peut faire des progrès dans ce domaine et obtenir les vérifications souhaitées, mais les messages d’erreur peuvent devenir très éloignés de la manière dont un développeur humain écrit le code, et l’implémentation est très pénible
L’expérience développeur est surprenante parce qu’il ne s’agit pas de « simples fonctions », mais d’une combinaison précise de génériques et de types associés. Je voulais utiliser des vérifications dans un style runtime, mais exécutées à la compilation ; pour y parvenir, il fallait toutefois écrire du code assez différent. Au final, rendre le Rust de compilation au niveau des types plus simple, plus fonctionnel et plus lisible pourrait être la voie pour que ce type de projet d’analyse formelle offre une bonne expérience aux mainteneurs comme aux utilisateurs. En résumé, je veux du Rust comptime. Et je me demande aussi si les Future basés sur Pin<&mut Self> sont déjà figés. J’aimerais expérimenter d’autres implémentations internes d’async/await, mais je ne sais pas par où commencer
1 commentaires
Avis de Hacker News
Bon article. Pour avoir déjà fait de la vérification de programmes, Rust me semble être le langage moderne le plus utile pour appliquer des méthodes formelles
Les règles de Rust éliminent beaucoup de cas difficiles à formaliser. Le gros problème restant est l’analyse des interblocages du point de vue des threads et du point de vue
Rc/emprunts, les deux étant dans une certaine mesure équivalents. S’il existait une analyse statique des interblocages en Rust, des pointeurs de déréférencement sûrs deviendraient probablement possibles ; et si l’on pouvait prouver que tous les appels borrow/upgrade ne peuvent pas échouer, on pourrait supprimer la plupart des comptages de références. On obtiendrait alors gratuitement la mutabilité interne quand c’est possibleLe gros problème des prouveurs de théorèmes, c’est qu’ils sont conçus par des gens qui aiment prouver des théorèmes : ils tombent dans le formalisme et leur sens de l’UI diverge de celui des programmeurs. La plupart des obligations de preuve peuvent être traitées par un solveur SAT, mais les problèmes difficiles nécessitent des outils plus lourds. Coq est trop manuel, et l’auteur juge ACL2 trop fonctionnel. Le machine learning peut aider à orienter un prouveur de théorèmes. Il est difficile de lui confier la preuve elle-même, mais inférer des plans de preuve dans du code où le flux de contrôle et l’usage des données se ressemblent globalement semble possible
Les routines cryptographiques de Firefox et Wireguard ne sont pas écrites en Rust, mais en F*, plus précisément en Low*, un DSL bas niveau intégré à F*, et elles sont entièrement vérifiées
https://project-everest.github.io/
https://mitls.org/
Le problème, quand on applique ce type d’outil à la vérification d’un langage externe comme Rust, c’est que les preuves ne sont pas écrites dans le langage cible, ce qui oblige les développeurs à apprendre deux langages. À partir de mon expérience sur Creusot, de mon travail sur Verus et Aeneas, et de mon expérience au laboratoire Why3, j’ai réfléchi à ce à quoi pourrait ressembler un « Rust pensé pour la vérification ». Si l’on concevait un tel langage dès le départ, sa facilité de vérification pourrait progresser par paliers par rapport à Rust, avec un impact particulièrement fort sur les parties difficiles des preuves
Ce qui me manque le plus dans les fonctionnalités de base, c’est l’équivalent de « lance quickcheck sur ma preuve ». Quand on a du code et qu’on essaie de prouver une propriété qui est fausse, il est facile de s’arracher les cheveux à comprendre pourquoi la preuve ne passe pas. Si, au milieu d’une preuve, on atteint un état absurde, ce serait bien qu’une commande du type « génère un contre-exemple à partir d’ici » en produise un. Les preuves sont très dépendantes du chemin suivi et ne sont généralement pas faciles, mais ces outils semblent tout proches de quelque chose de grand. Le processus consistant à prouver du code doit aussi refléter la possibilité que ce code contienne des bugs
Le prouveur ne produit pas de preuve incorrecte, il échoue simplement à dériver une preuve valide. Je ne pense pas qu’il existe beaucoup d’applications du machine learning ayant cette propriété
En réalité, en Rust, les verrous et le comptage de références sont des structures d’exécution.
Arccasse largement le modèle RAII de Rust, au point qu’il a fallu supprimer les scoped threads, dont le destructeur devait s’exécuter avant la fin de la portée. Le comptage global de références pose des problèmes de cycles et de fuites, et redevient un problème global. Il sera difficile de s’en passer complètement, mais je pense qu’il vaut mieux l’enfermer dans des portées de style arena. Les verrous semblent nécessiter des structures de données asymétriques, comme les canaux. En Go, on sépare un canal en émetteur et récepteur, et on peut faire undefer close(ch)dans la goroutine émettrice ; même en cas de panique, son exécution est garantie lorsque le reste du thread se termine. Il n’est pas nécessaire que ce soit des canaux, mais séparer les rôles lecture-écriture/producteur-consommateur rendrait le raisonnement beaucoup plus simple et aiderait aussi l’analyse formelleJ’aime bien le fait que cela parte d’une citation d’un article de Hoare vers 1973 et que cela se poursuive maintenant jusqu’à un deuxième billet. À l’origine, j’avais laissé un long commentaire dans le fil HN du billet de boat, en disant que faire pencher cette citation vers une perspective centrée sur Rust était compréhensible vu le parcours de boat, mais réduisait artificiellement la portée de la critique de Hoare
Grayson a maintenant pris ce fragment étroit comme point de départ pour discuter de quelques domaines et points de conception intéressants de Rust. Je pense toujours que mon commentaire était juste, mais la discussion issue du billet de Grayson a suffi à compenser mes réserves techniques sur le texte qui en était le point de départ
Depuis, avec l’apparition de techniques non sound plus avancées que le simple test, je pense que les méthodes non sound ont pris de l’avance sur les méthodes sound
Il avait identifié le problème et, avec le recul, la solution consistant à imposer par le système de types la mutabilité XOR partagée paraît n’être qu’un petit pas. Si l’on avait compris à l’époque que ce petit pas était la solution, on aurait évité 50 ans d’énormes souffrances
Mais la citation elle-même ne me semble pas renforcer ce point de vue. On peut y voir une tentative de prendre le regret plus général exprimé par Hoare sur l’existence sémantique même des références et de l’appliquer au modèle Rust d’état mutable non aliasé afin de contourner le problème. Mais cela revient plutôt à corriger un fragment étroit d’un problème plus vaste, puis à dire que tout le problème a disparu. Les parties omises, en particulier le début de la section « Variables » et l’exemple ALGOL 68, penchent beaucoup plus fortement vers l’idée que Hoare critiquait non pas seulement l’état mutable, mais le concept sémantique même de référence. Je reconnais que Rust tente de dompter une partie du problème, mais je ne pense pas qu’un langage quelconque l’ait « corrigé »
Je ne comprends pas très bien pourquoi ce billet reçoit autant d’éloges. J’ai l’impression qu’il balaie en un paragraphe plusieurs domaines de l’analyse de programmes. J’aime bien Graydon et je respecte son point de vue, mais ce paragraphe est beaucoup trop simplificateur
Dire que les langages avec GC ne se seraient pas vraiment dotés d’un solide support du raisonnement local est un homme de paille. Il y a eu des langages comme Pony, qui mettent des régions dans le système de types tout en utilisant un GC. Il existe aussi tout le domaine de l’analyse de pointeurs et de l’analyse d’échappement, qui infèrent l’unicité et déterminent si deux références peuvent être des alias. Le cœur du typage statique consiste aussi, via les classes et les champs, à diviser le tas en parties qui ne s’aliasent pas mutuellement. On ne parle pas de JavaScript, et il ne faut pas faire comme si Java/C#/Scala et d’innombrables langages avec GC n’avaient aucun raisonnement local sur l’état mutable
Les classes et les champs ne fournissent pas un raisonnement local complet sur l’état mutable. En effet, une classe/un objet A peut finir par dépendre de l’état mutable d’une classe/d’un objet B. L’héritage de classes à la Java ajoute lui-même davantage de complexité à mesure que le programme évolue dans le temps
Il existe bien sûr des contre-exemples, mais si l’on regarde les langages généralistes grand public avec GC comme Java, C# ou Python, c’est exact. On peut interpréter l’idée originelle de l’orienté objet comme proche de l’actor model actuel, avec des structures de données possédées que l’on ne modifie que par passage de messages. Mais les implémentations réelles de l’orienté objet sont loin d’approcher cet objectif. Java n’empêche pas de stocker des références mutables au même objet dans plusieurs objets. Ce billet explique mieux ce point : https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Édition : j’ai mal lu une double négation. Même en relisant, cela reste confus pour moi. Cela veut-il dire que Java, contrairement à JavaScript, dispose d’un raisonnement local ?
J’aime généralement les billets de Graydon, mais celui-ci, comme beaucoup de textes sur les méthodes formelles, peut induire en erreur les lecteurs qui ne connaissent pas le domaine. C’est un peu comme dire que la manière de transformer le plomb en or s’est améliorée d’un ordre de grandeur à un seul chiffre, sans préciser qu’il manque encore 29 ordres de grandeur pour que ce soit rentable en pratique
Est-ce que l’absence d’alias facilite beaucoup la vérification formelle ? Oui. Est-ce que cela permet pour autant de vérifier des programmes réels de manière pratique et économiquement efficace ? Pas du tout. Il existe des programmes, des circuits et des composants vérifiés formellement au quotidien, mais ils relèvent plutôt de l’exception, sont relativement très petits et sont conçus d’une manière particulièrement prudente. Les propriétés qui aident au raisonnement local sont importantes, mais elles ne changent pas vraiment la façon de garantir, de manière rigoureuse, la correction des logiciels grand public
Même les programmes écrits dans un langage très éloigné de la complétude de Turing — sans tas, sans pointeurs, sans entiers, avec seulement des variables booléennes, et dont les boucles ne peuvent pas s’exécuter plus de deux fois — ne peuvent pas être vérifiés de façon pratique, car ils se réduisent à TQBF. Pour certaines propriétés, par exemple la sûreté mémoire, c’est possible, mais cela ne suffit pas à ce dont les logiciels ont besoin. Dans les années 1970 à 1990, on espérait que, même si la complexité dans le pire cas était ingérable, les garanties locales et la structure des langages permettraient d’éviter ce pire cas ; depuis, il a été démontré que ce n’était pas le cas. L’espoir que les programmes réellement écrits par les humains soient suffisamment éloignés du pire cas pour permettre de bonnes heuristiques ne semble plus tenir non plus
Il existe une présentation sur le sujet : https://pron.github.io/posts/correctness-and-complexity
Le résultat essentiel est que la plupart des propriétés intéressantes que l’on voudrait vérifier ne se composent pas. Même si l’on prouve la propriété pour chacun des composants P1...Pn, le coût de prouver cette propriété pour P1 ○ ... ○ Pn ne croît pas seulement de façon superpolynomiale en n, mais aussi de façon superpolynomiale par rapport à la taille de chaque composant. Autrement dit, c’est aussi difficile que si l’on n’avait rien découpé, et la correction ne se décompose pas. C’est pourquoi « on peut vérifier pas mal de choses » et « ce qui est vérifiable n’est qu’une goutte d’eau dans l’océan » sont simultanément vrais, et cet écart est souvent absent des discussions sur les méthodes formelles
Ce n’est pas totalement faux, mais ce n’est pas totalement juste non plus. Il est étonnant que, malgré les nombreuses occasions qu’ont eues les personnes intéressées par ce sujet de le montrer au fil de ces centaines de répétitions, ta position n’ait absolument pas évolué. Cette attitude donne l’impression d’une fermeture maladive et finit par faire perdre leur temps à tous ceux qui participent à la discussion
Ce schéma se répète. Même pendant que des méthodes solides connaissent des améliorations importantes, des méthodes non solides réalisent en pratique des progrès bien plus grands vers des logiciels plus corrects. Un exemple très récent est https://antithesis.com. Bien sûr, dans certaines situations, les techniques solides peuvent être plus puissantes et plus pratiques ; c’est donc un sujet complexe
unsafe. Rien que cela serait vraiment utileJe viens aussi de laisser un commentaire connexe sur le billet consacré à F*. À en juger seulement par la syntaxe, je préfère subjectivement F*/F# à Rust, mais pour le logiciel de contrôle de spectacle que je développe, j’ai décidé d’utiliser Ada/SPARK2014
Pour que Rust attire le même type de personnes qu’Ada/SPARK2014, il lui faut une norme officielle publiée, comme les langages existants tels que C, Common Lisp, Prolog, Fortran ou COBOL. Rust commence à y entrer, avec la collaboration d’AdaCore et de Ferrous Systems pour proposer des outils de vérification formelle pour Rust comme pour Ada/SPARK2014, mais il n’existe pas encore de norme publiée, et l’héritage d’Ada et de SPARK2014 est immense
Il est intéressant de voir le comptage de références comme une sorte de GC optimisé à exécution immédiate, qui fonctionne lorsqu’on l’utilise strictement pour des données acycliques ou lorsqu’on peut accepter les fuites dues aux cycles. Python utilise l’approche hybride comptage de références + traçage décrite dans l’article, et j’ai aussi vu des déploiements en production où l’on forçait le collecteur par traçage à ne s’exécuter qu’une fois tous les N requêtes
Perl repose sur du comptage de références pur, mais dispose de références faibles, ce qui permet de rendre les données acycliques du point de vue du comptage de références, au prix de devoir faire attention aux parties d’une structure cyclique dont on conserve les références. Koka utilise en théorie le comptage de références, mais essaie en pratique d’en déplacer autant que possible à la compilation ; si, dans
y = x + 1, il est garanti quexn’a qu’une seule référence et ne sera plus utilisé ensuite, il peut réutiliser le même stockage pouryet effectuer une modification en placeNim propose ORC, qui ajoute au comptage automatique de références une implémentation de l’algorithme Recycler de Bacon+Rajan. Cet algorithme est conçu pour ne collecter que les cycles dans les systèmes fondés sur le comptage de références, et il est assez rapide. Pour revenir à Rust, on trouve ici une implémentation stop-the-world de Recycler : https://github.com/fitzgen/bacon-rajan-cc et elle est publiée sous forme de crate bacon-rajan-ccc dans ce fork : https://github.com/mbartlett21/bacon-rajan-cc La section Alternative du README contient des liens vers d’autres expérimentations dans le même domaine. Si l’article Recycler est difficile à trouver, j’en ai rassemblé des copies sous https://trout.me.uk/gc/, et si vous avez des goûts similaires, les articles sous https://trout.me.uk/lisp/ pourraient aussi vous plaire
La vérification formelle des programmes me rend impatient. La preuve qu’un programme implémente correctement une spécification est intéressante en théorie, mais peu utile en pratique
Écrire une spécification correcte est aussi difficile que programmer correctement : le problème difficile n’est donc pas résolu, seulement déplacé. Les méthodes formelles ont des usages pratiques, mais on les rencontre rarement
Une fois qu’on peut faire cela, on peut l’imposer comme précondition. Par exemple, devoir montrer qu’un tableau est déjà trié avant de le passer à une fonction
Le texte a été écrit le 15 mai 2024, jour du 9e anniversaire de Rust 1.0
J’ai lu l’article de Boats mis en lien, et il était excellent. J’ai été surpris de voir que la citation de Hoare, vieille de 50 ans, reste pertinente et qu’elle est aussi bien formulée
J’aimerais pouvoir utiliser quelque chose de plus simple, comme des type guards à la compilation. Quand les trait bounds prolifèrent, les programmes au niveau des types deviennent difficiles à lire
Par exemple
Where <<::Output as G>::Output as H>::Output: HList + Zoutype Output = <<::Output as G>::Output as H>::Output;. On y ajouteCons>>>, puis on se rend compte que des nombres commeU8de TypeNum sont eux-mêmes des imbrications deCons>>. On peut faire des progrès dans ce domaine et obtenir les vérifications souhaitées, mais les messages d’erreur peuvent devenir très éloignés de la manière dont un développeur humain écrit le code, et l’implémentation est très pénibleL’expérience développeur est surprenante parce qu’il ne s’agit pas de « simples fonctions », mais d’une combinaison précise de génériques et de types associés. Je voulais utiliser des vérifications dans un style runtime, mais exécutées à la compilation ; pour y parvenir, il fallait toutefois écrire du code assez différent. Au final, rendre le Rust de compilation au niveau des types plus simple, plus fonctionnel et plus lisible pourrait être la voie pour que ce type de projet d’analyse formelle offre une bonne expérience aux mainteneurs comme aux utilisateurs. En résumé, je veux du Rust
comptime. Et je me demande aussi si lesFuturebasés surPin<&mut Self>sont déjà figés. J’aimerais expérimenter d’autres implémentations internes d’async/await, mais je ne sais pas par où commencer