Licence CC BY-SA

Pourquoi la recherche en langage de programmation ?

Je fais de la recherche en langages de programmation. Dans ce billet j’explique pourquoi et comment, en essayant d’être accessible pour des gens qui connaissent peu (ou mal) la programmation et/ou la recherche.

Pourquoi la recherche en langages de programmation ?

Les programmeurs et programmeuses ont inventé de nombreuses représentations symboliques des programmes qui sont exécutés par un ordinateur, représentations que l’on appelle langages de programmation. On peut les voir comme des langages utilisés pour parler avec l’ordinateur, un programme étant un texte dans ce langage, le code source. Mais il est important de se souvenir que la programmation est aussi une activité sociale: la plupart des programmes sont écrits par plusieurs personnes travaillant ensemble, et les programmes écrits par une personne seule sont souvent réutilisés, inspectés et modifiés par d’autres. Un programme transmet une intention à l’ordinateur, mais il la communique aussi à des humains.

Quand on programme, on est facilement irrité par les défauts du langage de programmation qu’on utilise; il est très difficile de concevoir un bon langage de programmation. On lui demande au moins les trois qualités suivantes :

  • la concision: Les tâches simples doivent être décrites par des programmes simples, pas par des programmes gros ou complexes. Les tâches complexes nécessitent des programmes complexes, mais la complexité du programme doit venir uniquement du domaine métier (les spécificités de la tâche requise), sans complexité incidente imposée par le langage de programmation.

    Par exemple, les premières recherches en intelligence artificielle ont révélé le besoin d’un bon support, par le langage de programmation, du backtracking (retour en arrière) : annuler une série de décisions prises pour atteindre un certain but, en cas d’échec, pour commencer à nouveau selon une méthode différente. Certains langages de programmation rendent beaucoup plus facile d’exprimer cela que d’autres.

  • la clarté: En lisant le texte d’un programme, il faut qu’il soit facile de comprendre l’intention des personnes qui l’ont écrit. On dit qu’un programme a un bug (un défaut de fabrication) quand sa signification (pour l’ordinateur) ne correspond pas à l’intention de ses auteurs – une erreur a été faite pendant la transcription des idées dans le texte du programme. La clarté est un composant essentiel de la sûreté (éviter les comportements inattendus et dangereux). Pour l’améliorer, certaines constructions des langages de programmation nous aident à exprimer notre intention, et les concepteurs et conceptrices de langages de programmation travaillent à concevoir des outils pour vérifier automatiquement que l’intention ainsi exprimée est cohérente avec le reste du texte du programme.

    Par exemple, l’un des pires problèmes de sécurité découvert en 2014 (le fait que tous les ordinateurs et téléphones Apple ne vérifiaient pas correctement l’authenticité des sites webs demandant une connection sécurisée) était causé par une ligne dans le texte d’un programme qui avait été dupliquée – écrite deux fois au lieu d’une seule. La différence entre l’intention du programmeur (vérifier l’authenticité des communications sécurisées) et le comportement réel du programme (permettant à des mauvais acteurs de se faire passer pour votre banque ou boîte email, intercepter vos paiement en ligne, etc.) était considérable, et pourtant ni les humains ni les outils automatiques qu’ils utilisaient n’avaient repéré cette erreur.

  • la cohérence: Un langage de programmation devrait avoir une structure très régulière, pour qu’il soit facile pour ses utilisateurs et utilisatrices de deviner comment utiliser les parties du langages qu’ils ne connaissent pas encore bien. En particuliar, la cohérence aide la clarté : retrouver l’intention derrière le texte du programme demande une bonne connaissance du langage, et plus le langage est cohérent, prévisible, plus faibles sont les risques de mécompréhension. C’est un cas particulier d’un principe de conception plus général, le principe de surprise minimale.

Bien sûr, la liste (non exhaustive) ci-dessus n’est que l’opinion informelle d’une personne pratiquant la programmation (moi-même), et non pas une affirmation scientifique établie rigoureusement. La programmation est un domaine riche qui met en jeu de nombreuses activités, donc la recherche scientifique sur les langages de programmation peut être entreprise, et devrait être entreprise, depuis de nombreux angles différents. Entre autres, les mathématiques (la formalisation), l’ingénérie, le design, les interfaces homme-machine, l’ergonomie, la psychologique, la linguistique, les neurosciences, la sociologie, et les personnes qui pratiquent la programmation ont toutes leur mot à dire sur comment concevoir de meilleurs langages de programmation.

Pour ma part, je travaille au sein d’une communauté scientifique qui utilise la formalisation mathématique comme son principal outil pour étudier, comprendre et améliorer les langages de programmation. Pour travailler sur un langage, on lui donne une sémantique formelle (ou plusieurs) en définissant les programmes comme des objets mathématiques, au même titre que les nombres ou les fonctions. La sémantique d’un langage est alors donnée par une relation (mathématique) entre les programmes et leur comportement. On peut ainsi prouver des théorèmes sur les langages de programmations eux-mêmes, ou sur les analyses et transformations de programmes.

Voir dans le détail comment la formalisation mathématique d’un langage de programmation peut guider sa conception est absolument fascinant – c’est une approche très abstraite d’une activité très concrète. Ma communauté de recherche a défini un certain nombre de propriétés qui peuvent s’appliquer ou non à la formalisation mathématique d’un langage donné (l’objet mathématique que l’on a défini pour représenter le langage), et qui capturent certains aspects de l’utilisabilité du langage. Il s’agit en quelque sorte d’un ensemble de tests pour évaluer un langage. Cet ensemble de tests évolue au fil du temps, car nous affinons notre compréhension de ces propriétés formelles et nous en proposons de nouvelles, à partir de nos expériences d’utilisation des langages existants ou expérimentaux.

Avoir une sémantique formelle d’un langage que l’on étudie est une façon de comprendre ce que les programmes de ce langage veulent dire, ce qui est une première étape nécessaire pour évaluer ou améliorer la clarté du langage – un programme ne peut pas être clair si on ne commence pas par se mettre d’accord sur ce qu’il veut dire. Construire cette formalisation est un travail difficile (technique) et chronophage, mais son pouvoir de simplification ne peut pas être surestimé. Le travail de formalisation agit comme une loupe qui grossit les irrégularités, et suggère naturellement des changements du langage qui peuvent améliorer drastiquement sa cohérence. Il nous encourage à construire (ou reconstruire) le langage autour d’un petit ensemble de concepts centraux et indépendants, ses briques de base – c’est la meilleure façon de rendre la formalisation plus facile. Il peut donc améliorer aussi la concision, puisque des concepts avancés peuvent être décrits de façon simple en combinant ces briques de base. Bien sûr, trouver les bonnes briques de base demande une connaissance du domaine métier (celui des programmes dont on veut améliorer l’écriture dans ce langage); pour avoir des idées vraiment nouvelles il faut souvent explorer avec des prototypes ou faire des études d’usage, en dehors de l’activité de formalisation. La méthode de conception de langages que je préfère, c’est donc la co-évolution d’un langage et de sa formalisation, les activités de formalisation et de programmation ayant lieu en même temps, pour informer et diriger le processus de conception.


22 commentaires

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.

+0 -0

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. :)

+1 -0

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 ?

+0 -0

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. :)

Situphen

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.)

+4 -0

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 :)

+2 -0

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 ça1. 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…


  1. J’ai regardé ce que c’était sur Wikipédia, et je pense avoir compris l’idée, pourtant. 

+0 -0

@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".

+0 -0

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 programmation1, 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 mauvais2.


À 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.


  1. Ce qui est un peu atterrant, reconnaissons-le. 

  2. J’ai assez de curiosité pour chercher à comprendre (sinon je ne discuterai pas sous ce billet), et j’ai d’ailleurs essayer à l’occasion de comprendre des logiques de programmation se voulant meilleure (Rust, OCaml, notamment), mais je me suis toujours pris un mur, et je garde l’impression qu’il y a un monde entre ce que je suis techniquement capable de faire ou d’apprendre en un temps raisonnable (j’entends par là plusieurs dizaines d’heures, pas 5 minutes), et ce qui est nécessaire pour comprendre les logiques en question. 

+0 -0

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.
+5 -0

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 ?).

Gabbro

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

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

Ksass`Peuk

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).

+0 -0

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.

+0 -0

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.

+0 -0

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).

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.

gasche

Ç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.

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.

Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte