Quelques notes sur les alias mutables et la vérification des types en Rust

Rien à résumer.

[GN⁺]

Commentaire Hacker News

Résumé des commentaires de Hacker News

• Rust et les méthodes formelles

  • Rust semble être l’un des langages modernes les plus utiles pour appliquer des méthodes formelles.
  • Les règles de Rust éliminent de nombreux cas difficiles à formaliser.
  • Le principal problème restant est l’analyse des interblocages ; si une analyse statique des deadlocks était possible en Rust, on pourrait aussi obtenir des backpointers sûrs.
  • Le machine learning pourrait aider à guider les démonstrateurs de théorèmes.

• Citation de l’article de Hoare de 1973

  • Réduire la critique de Hoare à une perspective centrée sur Rust est artificiel.
  • La discussion de Grayson est suffisamment intéressante pour dépasser les réserves techniques.

• Critique de l’analyse de programmes

  • Ce texte passe à côté de l’ensemble du domaine de l’analyse de programmes.
  • Des langages comme Java ont un GC, mais offrent peu de support solide pour le raisonnement local.
  • L’analyse de pointeurs et l’analyse d’échappement peuvent inférer l’unicité et déterminer si des références sont distinctes.

• Scepticisme sur la vérification formelle

  • La vérification formelle est intéressante en théorie, mais rarement utilisée en pratique.
  • Écrire une spécification correcte est aussi difficile qu’écrire un programme correct.

• F et Ada/SPARK2014*

  • La syntaxe de F* est préférée, mais Ada/SPARK2014 est utilisé pour les systèmes de contrôle liés à la sécurité.
  • Rust n’a pas encore de standard officiel, ce qui rend difficile d’attirer le même type d’utilisateurs qu’Ada/SPARK2014.

• Limites des méthodes formelles

  • L’absence de références facilite la vérification formelle, mais ce n’est pas une méthode de vérification pratique ni rentable.
  • La plupart des programmes sont difficiles à vérifier formellement.

• Comptage de références et garbage collection

  • Python utilise un hybride de comptage de références et de traçage.
  • Perl utilise un comptage de références pur, mais gère les structures cycliques via des références faibles.
  • Nim utilise ORC pour fournir un système rapide qui ne collecte que les cycles.

• 9e anniversaire de Rust

  • Célébration des 9 ans de Rust 1.0.

• Motif typestate

  • Les articles sur le motif typestate sont appréciés.

• Gardes de type à la compilation

  • Il serait souhaitable de pouvoir écrire plus simplement des gardes de type à la compilation.
  • Les messages d’erreur des programmes au niveau des types sont complexes et nuisent à l’expérience développeur.
  • Il faudrait rendre les fonctionnalités de compilation de Rust plus simples et plus fonctionnelles.

Ce résumé propose des points de vue variés et est structuré pour être facile à comprendre pour un ingénieur logiciel débutant.