Que font les concepteurs de langage pour décider ou prouver qu'une fonctionnalité particulière fonctionne correctement?

Je m'intéresse à la conception de langage et en général, je peux facilement raisonner sur des fonctionnalités largement connues (par exemple, héritage, polymorphisme, délégués, lambdas, captures, garbage collection, exceptions, génériques, variance, réflexion, etc.), leurs interactions dans un langage particulier, les moyens de les implémenter, leurs limites, etc.

Au cours des derniers mois, j'ai commencé à lire sur Rust, qui possède un système de propriété qui garantit la sécurité de la mémoire et la gestion des ressources déterministes en forçant les durées de vie des objets à être statiquement vérifiables. Du point de vue d'un simple utilisateur de la langue, j'ai pu prendre le système presque immédiatement.

Du point de vue d'un concepteur de langage, cependant, il m'a fallu un certain temps pour comprendre pourquoi les choses à Rust sont exactement comme elles sont. Je ne pouvais pas immédiatement comprendre le raisonnement derrière certaines restrictions du système de propriété, jusqu'à ce que je me force à proposer des cas qui violeraient l'intégrité d'un système s'il n'avait pas ces aspects.

Ma question principale n'a rien à voir avec Rust et sa propriété en particulier - mais n'hésitez pas à l'utiliser comme exemple dans vos commentaires / réponses, si vous en avez besoin.

Lorsque les concepteurs de langage conçoivent une nouvelle fonctionnalité, quelle méthodologie ou processus utilisent-ils pour décider que la fonctionnalité fonctionne correctement?

Par "nouveau", je veux dire que ce n'est pas quelque chose qui a déjà été testé dans les langues existantes (et donc l'essentiel du travail a été fait par d'autres designers). Par «fonctionne correctement», je veux dire que la fonctionnalité résout correctement le problème prévu et qu'elle est raisonnablement à l'épreuve des balles. Par "à l'épreuve des balles", je veux dire qu'aucun code ne peut être écrit dans la langue ou un sous-ensemble particulier de la langue (par exemple un sous-ensemble sans code "dangereux") qui violerait l'intégrité de la fonctionnalité.

• S'agit-il d'un processus d'essais et d'erreurs, dans le sens où vous proposez une forme simple de la fonctionnalité, puis essayez de trouver des moyens de la violer, puis de la corriger si vous la violez avec succès, puis répétez? Et puis, quand vous ne pouvez penser à aucune autre violation possible, vous espérez qu'il ne reste plus rien et l'appeler un jour?

• Ou existe-t-il un moyen formel de prouver (au sens mathématique du terme) que votre fonctionnalité fonctionne, puis d'utiliser cette preuve pour obtenir en toute confiance la fonctionnalité (ou la plupart du temps) dès le départ?

(Je dois mentionner que j'ai une formation en ingénierie, pas en informatique. Donc, si je manque quelque chose qui serait évident pour les CS, n'hésitez pas à le signaler.)

J'ai du mal à trouver la référence exacte pour le moment, mais il y a quelque temps, j'ai regardé plusieurs vidéos de Simon Peyton Jones , qui a été un contributeur majeur à la conception de Haskell. Il est un excellent orateur sur la théorie des types, la conception de langage, etc., et a de nombreuses vidéos disponibles gratuitement sur YouTube.

Haskell a une représentation intermédiaire qui est essentiellement du calcul lambda augmenté de quelques choses simples pour le rendre plus facile à travailler. Le calcul lambda a été utilisé et prouvé depuis qu'un ordinateur n'était qu'une personne qui calculait des choses. Un point intéressant que Simon Peyton Jones fait souvent est que chaque fois qu'ils font quelque chose de sauvage et de fou avec la langue, il sait que c'est fondamentalement sain quand cela se réduit finalement à cette langue intermédiaire.

D'autres langages ne sont pas aussi rigoureux, privilégiant plutôt la facilité d'utilisation ou de mise en œuvre. Ils font les mêmes choses que les autres programmeurs pour obtenir du code de haute qualité: suivez les bonnes pratiques de codage et testez-le à mort. Une fonctionnalité telle que la sémantique de propriété de Rust est à la fois beaucoup d'analyse formelle et de tests pour trouver des cas d'angle oubliés. Souvent, des éléments comme celui-ci commencent comme la thèse de doctorat de quelqu'un.

Donc, pour la conception du langage , il y a des preuves (ou des bugs). Par exemple, tapez systèmes. Types and Programming Languages est le livre canonique décrivant les systèmes de types et se concentre sur la preuve de l'exactitude et de l'exhaustivité du système de types. Les grammaires ont une analyse similaire et les algorithmes (comme le système de propriété que vous décrivez) ont le leur.

Pour l' implémentation du langage , c'est du code comme les autres. Vous écrivez des tests unitaires. Vous écrivez des tests d'intégration. Vous faites des revues de code.

La seule chose qui rend les langues spéciales, c'est qu'elles sont (presque toujours) infinies. Vous ne pouvez littéralement pas tester toutes les entrées. Et (idéalement) ils sont utilisés par des tonnes de gens, faisant des choses étranges et intéressantes, donc tout bug dans la langue sera finalement trouvé.

Pratiquement , relativement peu de langues utilisent des preuves pour vérifier leur fonctionnalité et se retrouvent avec un mélange des options que vous mentionnez.

La première chose et la plus difficile qu'un concepteur de langage doit prendre en compte lors de l'introduction de nouvelles fonctionnalités, est de garder son langage cohérent:

• comment l'intégrer dans la grammaire du langage sans casser le code existant (cela peut être prouvé mathématiquement)
• comment il se rapporte aux fonctionnalités existantes (par exemple, si vous avez des tableaux fixes indexés 0..n-1, vous n'introduirez pas de nouvelle fonctionnalité de tableau variable indexée 1..n) (c'est la partie artistique de la conception)
• comment la fonctionnalité peut être implémentée sur l'ensemble de la chaîne d'outils afin que la nouvelle fonctionnalité puisse être absorbée par l'écosystème, les outilleurs et les programmeurs (la faisabilité peut être démontrée avec une preuve de concept, mais la mise en œuvre complète est une approche similaire à la programmation)

Pour guider dans cette affaire, un concepteur s'appuie sur un ensemble de règles et principes de conception. Cette approche est très bien décrite dans " La conception et l'évolution du C ++ " de Bjarne Stroustrup , l'un des rares livres dédiés à la conception de langage. Ce qui est très intéressant, c'est de voir que les langues sont rarement conçues dans le vide, et le concepteur regarde également comment leurs langues ont implémenté des fonctionnalités similaires. Une autre source (en ligne et gratuite) est les principes de conception de la langue java .

Si vous regardez les débats publics des comités de normalisation, vous verrez qu'il s'agit davantage d'un processus d'erreur d'essai. Voici un exemple sur le module C ++ un tout nouveau concept à introduire dans la prochaine version du langage. Et voici une analyse rédigée après quelques changements de langue , pour évaluer son succès. Et voici le Java Community Process pour définir de nouvelles spécifications Java, comme une nouvelle API . Vous verrez que ce travail est effectué par plusieurs experts qui rédigent de façon créative un document de réflexion et une première proposition. Ces propositions sont ensuite examinées par une communauté / un comité plus large qui peut modifier la proposition pour assurer un degré plus élevé de cohérence.

Comment tester les fonctionnalités du langage de programmation? C'est une très bonne question, et je ne suis pas sûr que l'état de l'art soit à la hauteur.

Chaque nouvelle fonctionnalité peut interagir avec toutes les autres fonctionnalités. (Cela affecte le langage, les documents, les compilateurs, les messages d'erreur, les IDE, les bibliothèques, etc.) Les fonctionnalités se combinent-elles pour ouvrir une faille? Pour créer des cas de bord méchant?

Même les concepteurs de langage très intelligents qui travaillent dur pour maintenir la validité du type découvrent des violations telles que ce bug Rust . Le système de type de Rust n'est pas si évident pour moi, mais je pense que dans ce cas, la durée de vie de la valeur de piste du système de type signifie que le "sous-typage" à vie (sous-gammes) se heurte aux attentes en matière de sous-typage ordinaire, de contraintes, de références et de mutabilité, créant une échappatoire où une staticvie ref peut pointer vers une valeur allouée à la pile et devenir plus tard une référence pendante.

Par «fonctionne correctement», je veux dire que la fonctionnalité résout correctement le problème prévu et qu'elle est raisonnablement à l'épreuve des balles.

Pour les langages destinés à être des langages de production , c'est-à-dire utilisés par de nombreux programmeurs pour créer des logiciels de production fiables, "fonctionne correctement" doit en outre signifier résoudre correctement le problème prévu pour le public visé.

En d'autres termes, l' utilisabilité est aussi importante pour la conception de langage que pour d'autres types de conception. Cela implique (1) la conception de la convivialité (par exemple, connaître votre public), et (2) des tests de convivialité.

Un exemple d'article sur ce sujet est: «Les programmeurs sont des gens, trop , un langage de programmation et les concepteurs d'API peuvent apprendre beaucoup du domaine de la conception des facteurs humains».

Un exemple de question SE sur ce sujet est: La syntaxe d'un langage de programmation a-t-elle été testée en termes de convivialité?

Un exemple de test d'utilisabilité a envisagé d'étendre une fonctionnalité d'itération de liste (je ne me souviens pas dans quelle langue) pour prendre plusieurs listes. Les gens s'attendaient-ils à ce qu'il parcourt les listes en parallèle ou via le produit croisé? Les concepteurs du langage ont été surpris par les résultats des tests d'utilisabilité.

Des langages tels que Smalltalk, Python et Dart ont été conçus en mettant l'accent sur la convivialité. Clairement, Haskell ne l'était pas.