Grosso modo, le frontend décode le source pour en faire un code intermédiaire qui sera traduit dans le langage de destinataion par le backend.
Merci pour ces précisions. Si je comprends bien, il y a un langage intermédiaire (agnostique vis à vis du langage source) que cible le frontend, puis le backend part de cette représentation intermédiaire pour traduire vers le langage cible qui dépendra de l'architecture machine. C'est cela ?
Je te laisse troller sur les langages, je vois pas le rapport avec la compilation :)
C'est pas du troll, c'est une boutade. ;-) Même avec des emoticônes, le second degré ne passe pas sur linuxfr ?
Ce n'est pas, directement, en rapport avec la compilation, mais avec la fin du message de gasche. Et deux des langages qu'il cite (OCaml et Haskell) dérivent explicitement du lamba-calcul. D'ailleurs gasche est relecteur des patchs soumis sur le compilateur OCaml et a les droits de commit sur le dépôt, et Philipp Wadler est un des grands contributeurs au langage Haskell et l'implémenteur de generics en Java (ça c'est pour toi, il me semble que c'est le langage que tu utilises le plus; et dans la vidéo il explique d'où vient l'idée ;-).
En tout cas, la vidéo a bien un lien avec le thème du journal : quand on s'occupe de faire un langage et d'écrire un compilateur, il vaut mieux bien maîtriser la théorie. Et cette théorie, elle vient d'une source principale : la logique mathématique et la théorie de la démonstration. ;-)
Par contre, je me suis trompé pour la vidéo où il montre un extrait d'un article de Turing, c'est celle-ci (mais le contenu des deux conférences est similaire). L'article date de 1937 et l'abstract est :
Computability and lambda-definability
The identification of "effectively calculable" functions with calculable functions is possibly more convincing than an identification with the lambda-definable or general recursive functions. For those who take this view the formal proof of equivalence provides a justification for Church's calculus, and allows the "machines" qhich generates functions to be replaced by the more convenient lambda definitions
Enfin si tu ne vois pas le rapport à la théorie des langages (et donc in fine avec la compilation), c'est peut être que tu n'en connais que succinctement le contenu, ou que tu ne connais pas le contenu de philosophie kantienne. ;-)
Juste une illustration, dans un article de 1905, au cours d'une polémique qui l'opposait avec des logiciens comme Russell ou Hilbert, Henri Poincaré écrit en introduction :
Pour M. Couturat, la question n'est pas douteuse : ces travaux nouveaux ont définitivement tranché le débat, depuis si longtemps pendant entre Leibniz et Kant. Ils ont montré qu'il n'y a pas de jugements synthétiques a priori, que les mathématiques sont entièrement réductibles à la logique et que l'intuition n'y joue aucun rôle.
C'est ce que M. Couturat a exposé dans les articles que je viens de citer; c'est ce qu'il a dit plus nettement encore à son discours du jubilé de Kant, si bien que j'ai entendu mon voisin à demi voix : « on voit bien que c'est le centenaire de la mort de Kant ».
Puis continuant, à la fin de son introduction il émet une très très grande objection au travaux des logiciens qui lui étaient contemporains :
Nous venons d'expliquer l'une des conditions auxquelles les logiciens devait satisfaire et nous verrons plus loin qu'il ne l'ont pas fait.
Et pour cause : ils ne pouvaient pas la satisfaire; et cette impossibilité devait être prouvée, par Gödel, 26 ans plus tard1 sous le nom de théorème d'incomplétude ou, dans la version de Turing, indécidabilité du problème de l'arrêt.
Donc qui avait raison ? Kant et Poincaré ! ;-)
Tout ça pour dire : l'ordinateur, les langages de programmations, l'informatique, ce n'est pas venu du jour au lendemain dans la tête de Turing. Ça s'inscrit dans une tradition historique qui relève de la logique, de la philosophie et des fondements de mathématiques : c'est ça les bases théoriques des langages de programmation. ;-)
soit en 1931, c'est à dire 150 ans après la première édition de la Critique de la Raison Pure (1781) dans laquelle on trouve un énoncé analogue au théorème d'incomplétude (et donc au problème de l'arrêt). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Dommage alors
Posté par kantien . En réponse au journal LLVM se fait de vieux os ? La recherche pour rester jeune.. Évalué à 3.
Merci pour ces précisions. Si je comprends bien, il y a un langage intermédiaire (agnostique vis à vis du langage source) que cible le frontend, puis le backend part de cette représentation intermédiaire pour traduire vers le langage cible qui dépendra de l'architecture machine. C'est cela ?
C'est pas du troll, c'est une boutade. ;-) Même avec des emoticônes, le second degré ne passe pas sur linuxfr ?
Ce n'est pas, directement, en rapport avec la compilation, mais avec la fin du message de gasche. Et deux des langages qu'il cite (OCaml et Haskell) dérivent explicitement du lamba-calcul. D'ailleurs gasche est relecteur des patchs soumis sur le compilateur OCaml et a les droits de commit sur le dépôt, et Philipp Wadler est un des grands contributeurs au langage Haskell et l'implémenteur de generics en Java (ça c'est pour toi, il me semble que c'est le langage que tu utilises le plus; et dans la vidéo il explique d'où vient l'idée ;-).
En tout cas, la vidéo a bien un lien avec le thème du journal : quand on s'occupe de faire un langage et d'écrire un compilateur, il vaut mieux bien maîtriser la théorie. Et cette théorie, elle vient d'une source principale : la logique mathématique et la théorie de la démonstration. ;-)
Par contre, je me suis trompé pour la vidéo où il montre un extrait d'un article de Turing, c'est celle-ci (mais le contenu des deux conférences est similaire). L'article date de 1937 et l'abstract est :
Enfin si tu ne vois pas le rapport à la théorie des langages (et donc in fine avec la compilation), c'est peut être que tu n'en connais que succinctement le contenu, ou que tu ne connais pas le contenu de philosophie kantienne. ;-)
Juste une illustration, dans un article de 1905, au cours d'une polémique qui l'opposait avec des logiciens comme Russell ou Hilbert, Henri Poincaré écrit en introduction :
Puis continuant, à la fin de son introduction il émet une très très grande objection au travaux des logiciens qui lui étaient contemporains :
Et pour cause : ils ne pouvaient pas la satisfaire; et cette impossibilité devait être prouvée, par Gödel, 26 ans plus tard1 sous le nom de théorème d'incomplétude ou, dans la version de Turing, indécidabilité du problème de l'arrêt.
Donc qui avait raison ? Kant et Poincaré ! ;-)
Tout ça pour dire : l'ordinateur, les langages de programmations, l'informatique, ce n'est pas venu du jour au lendemain dans la tête de Turing. Ça s'inscrit dans une tradition historique qui relève de la logique, de la philosophie et des fondements de mathématiques : c'est ça les bases théoriques des langages de programmation. ;-)
soit en 1931, c'est à dire 150 ans après la première édition de la Critique de la Raison Pure (1781) dans laquelle on trouve un énoncé analogue au théorème d'incomplétude (et donc au problème de l'arrêt). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.