Pourquoi la recherche en langage de programmation ?

Yay! Enfin une tribune de @gasche \o/.

Je peux modestement corroborer les constats et affirmations de cet article avec ma propre expérience. Ça fait un petit moment maintenant que j’explore différentes manières d’écrire des spécifications formelles sur lesquelles on peut raisonner par la suite (avec un focus un peu plus important sur les propriétés de sécurité). Effectivement, la spécification et la vérifications poussent à explorer même les chemins les moins probables pour s’assurer que tout fonctionne bien. Ça coûte en temps et en énergie, après. Quand on se force à tout faire « proprement », on se rend compte de toutes les hypothèses implicites que l’on a inconsciemment en tête quand on raisonne sur des choses.

Billet très sympa ! J’aurais cependant aimé avoir un exemple de formalisation mathématique d’un langage de programmation, car dit comme ça c’est très abstrait et je n’ai toujours aucune idée à quoi ça ressemble.

Merci pour ce billet intéressant.

J’ai malheureusement du mal à voir le lien entre la première partie et la seconde : comment peut-on utiliser la formalisation mathématique d’un langage de programmation pour répondre aux besoins énoncés en début de billet ?

Personnellement, les seuls exemples qui me viennent à l’esprit quand on me parle de recherche en langage de programmation, c’est Coq et le dernier truc qui m’a-t-on dit est super en OCaml (et dont je n’ai pas compris mot).

Étant donné que c’est du très abstrait appliqué à du très concret, il n’y aurait rien d’étonnant à ce que ce soit encore exploratoire, mais aurais-tu un exemple de ce que ça peut donner ?

En regardant un peu au pif sur google, je suis tombé sur ce poly. Lire les 15 premières pages, t’aideront à voir à quoi cela peut ressembler. Tu peux aussi regarder de ce côté autre poly.

Enfin pour une approche plus complète, il y a un livre que je trouve excellent : Types and Programming Languages.

J’aurais cependant aimé avoir un exemple de formalisation mathématique d’un langage de programmation, car dit comme ça c’est très abstrait et je n’ai toujours aucune idée à quoi ça ressemble.

Ouais, je trouve aussi le texte trop sec/abstrait, et on pourrait mettre des exemples. Mais j’ai décidé de ne pas être trop perfectionniste et d’envoyer le truc en l’état – sinon on n’écrit rien.

Pour un exemple positif, le livre (disponible en ligne) Using, Understanding, and Unraveling The OCaml Language – From Practice to Theory and vice versa est une exploration à la fois théorique et pratique des langages fonctionnels à la Caml, c’est-à-dire qui mélange modèle mathématique et implémentation du langage. Je conseille aux gens qui savent lire un peu de Caml (pas besoin d’en écrire tous les jours au petit-déjeûner) de regarder le premier chapitre, qui contient justement un exemple de définition formelle d’un petit langage de programmation, "Core ML".

Pour un exemple négatif, la PEP 3104 qui a été acceptée en Python, et introduit le mot clé nonlocal:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

def make_scoreboard(frame, score=0):
    label = Label(frame)
    label.pack()
    for i in [-10, -1, 1, 10]:
        def increment(step=i):
            nonlocal score # ligne nécessaire ici
            score = score + step
            label['text'] = score
        button = Button(frame, text='%+d' % i, command=increment)
        button.pack()
    return label

Cette fonctionnalité est une merde qui est nécessaire parce que Python ne respecte pas les propriétés mathématiques basiques de la portée lexicale – et la raison pour ça c’est que Guido Van Rossum a commencé par un langage tout pourri, sans suivre aucun des principes de base de la théorie des langages de programmation déjà existante à l’époque, et l’a enrichi au fil du temps, mais forcément il y a des défauts de l’époque qui se voient encore aujourd’hui. (Globalement Guido pense que la recherche en langage de programmation ne sert à rien, et le langage s’en ressent. Ça rend aussi difficile pour des universitaires de travailler à améliorer le langage. C’est pour ça que la transition vers le typage optionnel qui a lieu en se moment est faite surtout avec les pieds.)

C’est pareil pour Coffeescript, dont la non-syntaxe de définition des variables locales est complètement merdique. Là c’est un cas un peu plus triste puisque plusieurs personnes (moi compris) sont allées essayer de convaincre le créateur du langage de changer d’avis, il n’a jamais voulu, et il y a des centaines d’utilisateurs qui se sont pris les pieds dans le tapis à cause de ça. (Maintenant ce langages est devenu complètement inutile avec l’évolution de Javascript et les utilisateurs migrent en sens inverse, bien fait!)

(Peut-être que la teneur des exemples ci-dessus donnent des indices sur la raison pour laquelle il n’y a pas tellement d’exemples dans le billet de départ. Ils sont plein d’opinions et assez clivants, et c’est difficile de ne pas mettre les gens sur la défensive quand on leur montre un point de design spécifique d’un langages qu’ils estiment en leur faisant remarquer que ce point spécifique est d’une laideur infâme.)

Passionnant.

Ca donne vraiment envie d’en savoir beaucoup plus, comme les gens ci-dessus l’ont dit.

Et notamment : "à quoi ça ressemble". A quoi on peut aboutir en menant un telle analyse d’un langage de programmation. Une grille "Bien" / "Pas bien". Une grille "Lisible" / "Peu lisible" / "Pas lisible". "Cérémonieux" / "Pas trop" / ? "Très error prone" / … / "Paranoïaque".

Pour quelqu’un comme moi développant quotidiennement sans avoir pu suivre dans son cursus de cours de théorie des langages (et qui le regrette profondément). Y’a des trucs qui me fascinent de jour en jour, ou qui m’interpellent.

Avoir un langage qui permet de faire, à la compilation, des équations aux dimensions. Genre "non, t’es en train d’ajouter des années lumières à des Kelvin, je compile pas", je trouve ça excellent. Apprendre ce qu’est une type class à quoi ça peut servir, et comment ça peut m’aider, c’est top.

Mais concrètement, sur l’échelle de "pénible" à "ça marche tout seul et y’a pas de bug", comment chacune de ces features, ou choix de design fait avancer le langage ? C’est ça que j’ai du mal à percevoir.

En tout cas merci beaucoup de nourrir la réflexion, plein de polys à ingurgiter

Ce que tu dis sur Python me donne un exemple concret de ce que ça peut apporter : j’ai récemment proposé un pseudo-cours de Python a des collègues (je suis doctorant en science, on est content quand les gens utilisent python plutôt que matlab) et plutôt que d’insister sur la syntaxe qu’ils trouveraient sans difficulté dans n’importe quel cours, j’ai parlé des questions de mutabilité et de portée des variables qui donnent des bugs assez horribles à comprendre, et dont peu de gens parlent réellement.

Effectivement, ce genre de chose fait partie des défauts de Python pour moi, et si la recherche peut aider à éviter ce genre de problème, ça vaut le coup de l’écouter.

Je suis en parallèle la discussion sur Linuxfr, et ça y parle beaucoup de type somme (présenté comme un truc de base). J’aurai une question bête : à quoi ça sert ? Perso, je fais surtout du Python, C++ et Fortran, et je vois mal l’intérêt de ça¹. En Python, on a le duck typing, donc on s’en fout, en C++, quel intérêt par rapport au polymorphisme, et en Fortran, il y a beaucoup de choses qui me manque (programmation générique simple), donc ça reste assez loin de mes priorités…

@Gabbro : Il est plus simple de faire du multiple-dispatch quand tu as des "sous-types" (parce que là ce n’en est pas du coup) qui sont très peu susceptible d’évoluer, là où en C++ tu sors nécessairement du visiteur ou std::variant qui imite ça en moins concis, tu as une mécanique directe dans le langage.

A noter que le plus adapté est sans doute le multi-méthodes mais je ne sais pas s’il existe beaucoup d’implémentation vraiment efficace de ça.

@gasche : oh, je me sens moins seul sur le forum, tu bosses sur quels outils ?

Pour compléter la réponse de Ksass`Peuk, gabbro tu peux regarder ici :

https://guide.elm-lang.org/types/union_types.html

Quand j’ai trifouillé des projets avec Elm par pure curiosité, c’est vraiment un truc qui m’a paru ultra pratique pour "du front".

Le premier exemple ressemble à de l’"enum on stereoids" donc pas forcément très convainquant. Par contre, le second exemple est déjà plutôt sympa. Quand t’as du pattern matching (+ destructuring derrière), t’as vraiment un gros panel à portée de main. Tu as réellement décrit ton problème en disant : un utilisateur c’est soit une personne anonyme qui pourrait potentiellement disposer de certains attributs, ou d’une personne nommée, avec d’autres attributs, ou peut-être même qu’ils en ont en commun.

Du coup, avec ton pattern matching, tu peux dire "dans le cas où c’est un anonyme, je sais qu’il a tel ou tel attribut, dans le cas où il est nommé j’ai son nom, et dans le cas ou je ne sais pas, peut-être que je peux faire des trucs avec les attributs qu’ils ont en commun, sans nécessairement introduire de hierarchie de type entre les deux".

Ksass`Peuk, je crois que tu viens de résumer pourquoi j’ai du mal à voir l’intérêt direct ce domaine : je n’ai pas compris un traitre mot de ce que tu racontes (multiple-dispatch ? visiteur ? std::variant ?).

Et pourtant, dans mon environnement immédiat, je fais partie des bons en programmation¹, et de manière plus générale, pour quelqu’un qui fait ça en loisir ou comme simple outil de travail (et non comme but), je pense ne pas être mauvais².

À Javier : Quel intérêt par rapport à de la programmation orienté objet de base ? Tu as un objet User, avec une version instanciée par défaut, et une version instanciée avec un paramètre. C’est peut-être un peu plus verbeux avec un objet, mais je ne vois pas en quoi c’est conceptuellement différent.

Un type somme apparaît naturellement quand on a une donnée qui passe à un point du programme et qu’il est naturel de décrire comme "soit un A, soit un B, soit un C, mais rien d’autre". Ça arrive vraiment tous les jours et une fois qu’on connaît l’idée on la reconnaît partout.

Par exemple (j’essaie de deviner un exemple qui te parle selon les langages que tu cites!) je peux vouloir dire qu’une matrice est représentée soit comme une matrice dense, soit comme une matrice sparse. Imagine que j’ai déjà un type dense_matrix et sparse_matrix. Je peux construire le type somme matrix, qui contient ces deux cas. Il faut que je choisisse un nom à donner à chaque cas (mettons tout simplement Dense et Sparse):

1
2
3

type matrix =
| Dense of dense_matrix
| Sparse of sparse_matrix

Maintenant je peux faire des opérations qui prennent en entrée une matrice "soit dense soit sparse" et qui fait la bonne chose. Au hasard:

1
2
3
4
5

let add m1 m2 = match m1, m2 with
| Dense d1, Dense d2 -> Dense (add_dense d1 d2)
| Sparse s1, Sparse s2 -> Sparse (add_sparse s1 s2)
| Dense d1, Sparse s2 -> Dense (add_dense d1 (densify s2))
| Sparse s1, Dense d2 -> Dense (add_dense (densify s1) d2)

En fait on peut fusionner les deux derniers cas

1
2
3
4

let add m1 m2 = match m1, m2 with
| Dense d1, Dense d2 -> Dense (add_dense d1 d2)
| Sparse s1, Sparse s2 -> Sparse (add_sparse s1 s2)
| (Dense d, Sparse s) | (Sparse s, Dense d) -> Dense (add_dense d (densify s))

Remarques:

• le code que j’ai écrit est concis et simple
• le compilateur vérifie pour moi que je n’ai pas oublié un cas (puisqu’il sait qu’aucun autre cas n’est possible); si j’oublie une des lignes, j’ai un warning ou une erreur.

Le multiple dispatch c’est le problème auquel tu es confronté quand tu as un traitement qui dépend du type réel de plusieurs instances. Quand on a qu’une seule instance qui définit le traitement, on fait ça :

1
2
3

struct A{
  virtual void foo() = 0; //on va avoir un dispatching en fonction du type réel de A uniquement
};

Le traitement ne dépend que de this : c’est un simple dispatch. Maintenant, là où ça commence à être le bazar, c’est si on transforme un peu le problème en :

1
2
3

struct A{
  virtual void foo(A& a) = 0;
};

Où le choix du traitement ne dépend plus seulement de this mais aussi de a, on est sur un double dispatch. Et après on peut pousser avec 3, 4 , 5 instance : multiple disptach. Et c’est le problème par exemple auquel on est confronté quand on s’attelle au Javaquarium proposé sur le forum comme exercice pour l’objet .

Et la méthode de résolution en objet, c’est d’utiliser quelque chose qui ressemble au patron de conception visiteur (mais spécialisé pour la tâche qu’on veut résoudre). Seulement niveau usine à gaz, le visiteur, c’est pas du flan.

Pour ce qui est de std::variant, c’est l’implémentation des types sommes en C++. Sauf que certaines facilité ne sont pas présentes (car elles devraient être ajoutées au niveau du langage et pas comme bibliothèques) et du coup, ce n’est pas aussi simple à manipuler que dans les fonctionnels ou grosso-modo on va écrire :

1
2
3
4
5

match dep1, dep2 with
| cas11, cas12 -> traitement
| cas11, _ -> traitement
| _, cas22 -> traitement
| _, _ -> traitement

Merci beaucoup pour vos réponses.

Je travaille sur OCaml, à moitié comme hobby, et sinon je fais des trucs théoriques (du lambda-calcul simplement typé, un zeste de théorie de la démonstration, et ces derniers temps j’essaie de comprendre les solveurs SAT).

Ok, donc surtout du fondamental. Si tu t’ennuies j’aurai bien besoin d’un équivalent des solveurs SAT mais pour la logique de séparation .

http://fbinfer.com/ ?

C’est une question intéressante mais je n’y connais pas grand chose; les gens de Why3 ont du réfléchir à ces questions-là, enfin plein d’autres gens aussi puisque c’est un sujet chaud. Moi, à une échelle beaucoup plus modeste, j’essaie juste de découvrir SAT – j’en parlerai peut-être par ici à l’occasion.

Il me semble que c’est une forme d’interprétation abstraite avec de la logique de séparation dans Infer. Verifast transforment des propriétés en logique de séparation vers des formules SMT. Ce qui serait super, ce serait de directement manipuler des formules en logique de séparation .

Salut

Est-ce que les bonnes pratiques, idiomes, sémantiques, principes de conception, etc. font partie du domaine de recherche ? Est-ce que l’ensemble de ces "règles" (ou une partie safe d’un langage non safe) est étudié comme si c’était un nouveau langage ?

Est-ce que l’apprentissage fait aussi partie du domaine du recherche ? Pour éviter par exemple qu’un langage soit très bon sur le papier, mais qu’il soit mal compris en pratique. Ou, pour un langage permissif (ie qui autorise plusieurs solutions pour une problématique, chaque solution étant plus ou moins qualitatif) que les apprenants comprennent bien les syntaxes à utiliser ou non.

Est-ce que l’ensemble de ces "règles" (ou une partie safe d’un langage non safe) est étudié comme si c’était un nouveau langage ?

C’est une question intéressante. Souvent la réponse est malheureusement "non", mais il y a des cas où c’est fait :

• certains outils se limitent à un sous-ensemble du langage plus facile à traiter, et parfois ça coincide à des sous-ensembles que certaines communautés s’imposent; par exemple le C sans allocation dynamique ni récursion correspond bien aux normes de l’embarqué, ou "javascript sans eval" au bon sens.
• il y a des sous-ensembles spécifiques qui ont été spécifiés soigneusement, je pense à SPARK Ada par exemple comme un sous-ensemble de Ada.

Est-ce que l’apprentissage fait aussi partie du domaine du recherche ? Pour éviter par exemple qu’un langage soit très bon sur le papier, mais qu’il soit mal compris en pratique.

On pourrait faire de la recherche sur l’apprentissage, dans le cadre d’une collaboration avec des chercheurs qui connaissent les méthodologies nécessaires (très différentes de celles décrites dans ce billet) : user studies (comment collecter des retours de façon rigoureuse), statistiques (pour traiter correctement les données), etc. C’est un aspect peu exploré parce que très difficile à mettre en place. Le seul cas qui se fait relativement souvent c’est des études semi-rigoureuses sur des classes d’étudiants à l’université en situation d’apprentissage.

En pratique mon expérience est que les chercheurs ont une bonne intuition (tirée de leur pratique personnelle du langage) de ce qui va coincer, paraître compliqué pour d’autres utilisateurs. Je n’ai pas connaissance de cas où une idée paraissait une super simplification du point de vue des mathématiques, mais s’est révélée mauvaise à l’usage.

Par contre, un aspect un peu lié et intéressant, c’est que la tolérance des utilisateurs à des aspects plus avancés du langage évolue avec le temps. C’est arrivé plusieurs fois qu’au moment de la conception d’un aspect d’un langage il y a 20 ans, les chercheurs ou chercheuses se disent (à raison) : "la version la plus générale est trop riche et va perturber les utilisateurs, si on la restreint de telle façon on a un cadre plus simple qui va capturer la grande majorité des usages courants", mais qu’avec le temps la communauté évolue, s’habitue aux idées, et (15-20 ans après) demande la version la plus générale. C’est arrivé par exemple pour les types de rangée (row types) et les types de sorte supérieure (higher-kinded types).

Ça, c’est très intéressant. C’est un point à creuser, parce qu’il questionne la capacité des maths à décrire et à représenter le monde. Personnellement, je ne suis pas convaincu qu’il puisse exister une idée qui paraisse super du point de vue des mathématiques sous-jacentes, mais qui à l’usage ne tienne pas debout. Autrement, c’est que la formalisation est mauvaise.

J’ai l’impression que la bonne question à se poser, c’est de savoir ce que l’on peut mathématiser aujourd’hui en l’état actuel de la science, et si la représentation mathématique du langage est celle que l’on veut.

En tout cas, c’est un chouette billet.

Je pense que l’article Réminiscences d’un chercheur en informatique 1967-2000 devrait intéresser des gens.

Saroupille : bon texte en effet. J’ai mis un moment à comprendre que le terme "l-calcul" ne désigne pas une sorte de calcul ancienne et oubliée depuis, mais veut en fait dire "lambda-calcul" – c’est un peu dommage de ne pas avoir utilisé la formulation standard.