• [^] # Re: Super texte ...

    Posté par . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5. Dernière modification le 18 octobre 2017 à 11:16.

    Je comprend pas. Un programme écrit dans un langage donné est quelque part déjà un objet mathématique. « et à partir de cela définir le langage » euh, on commence pas par définir le langage avant d’écrire des programmes ???

    En mathématiques, pour décrire les ensembles de nombres (nombres entiers, relatifs, rationnels, réels, complexes...), on fait l'inverse. D'abord je définis ce qu'est un entier naturel n, et ensuite je définis l'ensemble des entiers \mathbb{N}. C'est pareil pour les programmes : d'abord je définis ce qu'est un programme que je veux étudier, et à partir de cela je peux définir le langage de programmation.

    Alors la façon dont je définis "un programme" c'est en donnant, par exemple, une syntaxe BNF qui, on est d'accord, correspond bien au choix d'un certain langage de programmation. Mais ce n'est pas à ce moment qu'on définit le langage, c'est seulement ensuite, une fois qu'on a défini ses programmes.

    Il y a une légère ambiguité dans le texte sur laquelle tu mets le doigt : quand je dis "programme", est-ce que je parle du code source du programme (facile à définir comme un objet mathématique), ou du comportement à l'exécution du programme (plus délicat à définir) ? Dans cette partie du texte, quand je parle de "voir un programme comme un objet mathématique", je parle plutôt du code source (ou d'une représentation plus abstraite mais de même genre), et c'est quand je parle de "sémantique" (ou "signification") du programme que je m'intéresse à la définition (formelle) du comportement à l'exécution.

    Par exemple dans le cas d'école du lambda-calcul, on définit d'abord un terme t du lambda-calcul (donné par une grammaire et une structure de nommage), c'est ce que j'appelle "définir un programme comme un objet mathématique". Ensuite on définit par exemple une relation de réduction petit-pas t_1 \to t_2, cela donne un modèle d'exécution pour les programmes et cela fait partie de la définition du langage comme un objet mathématique.

    J’imagine que par « mathématiquement » tu veux dire « dans un formalisme logique ».
    [..]
    Ton utilisation de « mathématique » me gène en fait, en tant que personne qui connaît un peu le domaine.

    Ce que j'appelle "objet mathématique" c'est un objet qui est défini dans le monde mathématique, pas dans le monde réel. L'adjectif "mathématique" désigne les concepts et objets qui vivent dans ce monde mathématique.

    Il y a une différence entre "un programme C", un concept du monde réel, et "l'objet mathématique qui représente un programme C dans mon formalisme". C'est plus facile à voir quand on pense à la différence entre "un processeur qui exécute des instructions assembleurs" et "l'objet mathématique qui définit la sémantique du processeur qui exécute l'assembleur" : on conçoit aisément qu'il peut y avoir une distance importance entre les deux (rayons cosmiques, attaque Row Hammer, etc., qui sont ou ne sont pas modélisés par l'objet mathématique dont on parle). Pour un programme C, la distance est plus petite voire nulle (en fait les programmeurs pensent à l'objet abstrait, pas à une séquence d'octets sur leur disque; mais ma modélisation mathématique ne rend pas forcément compte d'alloca, ou des extensions GNU machin, ou du préprocesseur, etc.). Je préfère garder systématiquement la séparation entre les deux mondes car elle est importante pour comprendre la portée des énoncés formels en général, et l'oublier peut conduire à des erreurs (dans les deux sens : trop promettre à partir d'une preuve formelle, ou alors critiquer une preuve hors de propos car on n'a pas regardé le modèle avec soin).