Justement, selon moi, le bouquin et l'article que je cite vulgarisent le sujet comme il faut : ils sont rapides à lire et pas vraiment techniques. Il se concentrent, notamment l'article, sur les concepts à l'oeuvre.
Tout l'inverse du bouquin amphigourique d'Hofstadter qui se concentre sur les aspects mécaniques de la numération de Gödel qui, je le répète, ne présente aucun intérêt. Le résultat de Gödel, ce n'est certainement pas qu'on peut représenter des lettres par des nombres ; ça c'est juste un artifice technique connu (c'est même comme ça que fonctionne un ordinateur, tiens tiens). L'approche d'Hofstadter, c'est un peu comme celui qui prétendait lire les grands événements du monde par des analyses de la valeur des lettres hébraïques dans le tanakh.
L'important, c'est la distinction entre démontrabilité et vérité, la diagonalisation, l'existence d'indécidables, l'absence ontologique de métalangage, les conséquences pour les maths et l'info...
Pas d'accord. Ce bouquin est un divertissement amusant mais n'a aucun intérêt scientifique. C'est plus de la numérologie qu'autre chose, de même qu'une fascination toute positiviste pour la sacro-sainte autoréférence qui a fait les choux gras de l'IA (dont Hofstadter est un thuriféraire).
Non c'est pas l'inverse.
Ça se voit très bien en prenant la contraposée de ton raisonnement qui serait :
x = y => f(x) = f(y)
ce qui est le moins qu'on puisse attendre d'une application !
Pour ma part, je ne connais personne qui ait payé pour publier dans une revue dans mon domaine (informatique). Là encore, il semble que c'est le cas pour certaines disciplines ou pour certaines revues particulières peut-être (celles qui sont plus des magazines que des revues, et plus à destination de la recherche privée, comme ce que publient l'ACM et l'IEEE en info, mais je n'en suis même pas certain).
Pour ce qui est de la biologie, je ne sais pas comment ça se passe, mais il faut savoir que les relecteurs ne sont en général pas rémunérés dans de nombreuses disciplines (ex: informatique).
En fait le problème principal réside dans le mapping données Caml <--> données CLR, notamment à cause du polymorphisme paramétrique (= généricité) de Caml. L'autre difficulté vient du sous-typage Caml qui est structurel et non pas pas noms.
Cf mailing-list Caml pour plein de posts à ce sujet.
Ça n'empêche pas qu'il est possible d'effectuer la compilation mais le code obtenu est d'une efficacité moyenne.
C'est bien ce que je dis: ces MV ont été développées avec l'idée qu'elle seraient la cible de langages impératifs à objets. Qu'il y ait des raisons objectives n'est pas le problème. Je trouve juste qu'il faut arrêter le trip "machine virtuelle universelle" (est-ce un déplacement du bon vieux "langage universel"?). C'est absurde. Mieux vaut plusieurs MV effectives pour des paradigmes précis qu'une seule MV moyenne dans tous les cas.
En l'occurrence, les MV pour Java et C# ne sont pas adaptées à la compilation des langages fonctionnels. Contrairement à ce que tu prétends, il ne s'agit pas juste de compiler vers du code itératif. Pour les langages fonctionnels, on utilise en général certaines techniques pour lesquelles on ne trouve pas de primitive adéquate dans les MV sus-citées, on est donc obligé de passer par des fonctions qui bouffent du temps CPU pour rien. La gestion de la mémoire dynamique est en particulier problématique. Y'a qu'à voir les difficultés pour compiler du OCaml ou du F# vers la MV C#.
Encore une fois je ne critique pas ces MV en tant que telles, je dis juste qu'elles ne constituent pas la solution "universelle".
Non non, j'objecte pas :-)
Je travaille grosso modo dans le domaine des langages de programmation et c'est donc un sujet qui m'intéresse. J'expose mon avis et mes doutes sur la question de la réflexivité, au sens large, comme paradigme (parmi d'autres) de programmation.
Tout à fait d'accord sur le fait que la réflexivité est plus facile à implémenter sur un interprète mais ça n'empêche que ça n'a pas de rapport avec le haut niveau supposé du langage.
Pareil pour l'indépendance par rapport au matériel. Rien n'interdit de développer une librairie abstrayant l'OS et de conserver le langage compilé. Évidemment, ça demande du travail mais c'est pas extrêmement compliqué.
Mais dans les deux cas, tout ça c'est le problème des concepteurs de l'environnement d'exécution et on peut se poser la question de leur qualité s'ils développent un interprète uniquement parce que c'est dur de faire un compilo et que c'est plus direct pour l'indépendance par rapport au mtériel. Je crains que ça ne soit souvent le cas de pas mal de langages interprétés de la communauté du libre.
Je pense qu'il serait completement incoherent pour des developpeurs de logiciel libre de batir une plate-forme sur une JVM alors qu'il existe une specification standard (ISO et ECMA) d'une machine virtuelle performante qui a ete concue de maniere a laisser aux developpeurs le choix du langage. http://www.ecma-international.org/publications/standards/Ecma-335.h(...)) . Quel que soit le langage utilise, le code source est compile en CIL (Common Intermediate Language).
Y'a quand même un problème : cette machine virtuelle, comme la JVM, et comme toute MV, a été développée avec certaines fonctionnalités en tête. En l'occurrence, elle a été prévue pour être la cible d'un langage à objets. Par contre, elle n'est pas adaptée à l'exécution des langages fonctionnels.
D'accord.
Donc, pour vous (/toi), un langage de haut niveau, ce serait un langage faiblement typé ou réflexif, par exemple?
Dans ce cas, on n'a pas du tout la même conception du haut niveau. Pour moi, un langage de haut niveau, c'est un langage qui a (au moins) les aspects suivants:
- syntaxe et sémantique opérationnelle claires et simples
- système de types fort et expressif
- abstraction importante par rapport à la machine.
La réflexivité entre-t-elle dans ce cadre? La question me semble mal posée (cf. (*) plus bas).
Ceci dit, la réflexivité ne fait pas forcément mauvais ménage avec un typage fort, contrairement à ce qu'on peut lire ici ou là. C'est vrai qu'on a intuitivement du mal à croire qu'on puisse les marier mais en fait, si (cf MetaOCaml, ou les langages à n niveaux).
Par ailleurs, l'implémentation du typage et de l'exécution sont fortement découplées en général, ou alors il y a un problème dans le langage.
J'admets par contre que c'est plus facile d'implémenter la réflexivité dans un interprète, vu qu'on programme ce dernier dans un langage gérant la mémoire à plus haut niveau que le microprocesseur.
(*) La réflexivité est un thème qui réapparaît souvent quand on parle des langages de programmation, et on dit souvent que c'est une fonctionnalité nécessaire. Ce qui m'étonne dans ce discours, c'est que la réflexivité n'est qu'une technique, qu'un moyen. Mais il est vrai que c'est assez fascinant, ce qui à mon avis occulte la réflexion (!) qu'il faut entreprendre.
La discussion ne devrait pas porter sur la réflexivité elle-même mais sur l'objectif auquel elle est censée répondre. Ce but, laissé souvent implicite, c'est en général la reconfiguration dynamique d'un programme, qui implique la génération et le chargement dynamiques de code. Or pour ça on n'a pas nécessairement besoin en pratique de toute la réflexivité.
Utiliser la réflexivité ex abrupto façon Lisp ou même Java, ça revient à contourner le typage (en passant par des quotes ou des chaînes de caractères).
Par contre, si on se concentre sur l'idée de reconfiguration dynamique, on peut trouver des primitives cloisonnées (contrairement à la réflexivité) qui suffisent à produire 99% des programmes (facilement 99% du temps) et qui bénéficient, elles, d'une sémantique abstraite (typage) claire et expressive.
Dans ces conditions, on a le beurre (la reconfiguration dynamique) et l'argent du beurre (la sûreté assurée par le typage fort).
Et oui, Java, c pas du C/C++, et c ca qu'est cool, maintenant, l'informatique a évolué et on peut se permettre de ne pas perdre son temps à penser à la mémoire qui reste : il y a même des gens pour dire que des langages interprétés sont bien car ils sont encore plus haut niveau que Java
Quel rapport entre l'interprété et le haut-niveau?
Je crois que tu ne comprends pas mon propos principal: personne ne prône rien puisque aucune université (publique) ne prend de décision "globale". À l'intérieur d'une université, tout le monde fait ses choix, selon les moyens financiers mis à disposition de tel ou tel enseignement et des opinions personnelles d'un individu.
Ensuite, permets-moi de te dire que la recherche, l'enseignement et l'administration des moyens (de l'enseignement et de la recherche) prennent suffisamment de temps pour en plus se taper un boulot de développement.
Historiquement, l'INRIA (à l'époque IRIA) a été fondé par De Gaulle pour assurer l'indépendance informatique de la France. Puis sa mission a évolué vers l'informatique plus fondamentale où il est maintenant au top niveau.
Si on estime que le LL est important dans un projet de société, alors ce serait à mon avis plutôt à l'Union Européenne de financer des centres de développement idoines. Mais ce n'est pas le boulot des chercheurs.
Pour ma part, je n'utilise que les LL pour des raisons éthiques (mon côté gauchiste), qualitatives (les LL aboutis sont souvent supérieurs sur le plan technique) et financières (je n'utilise que des LL gratuits, ça me coûte moins cher dans mon travail et ma vie personnelle).
Maintenant, sur le plan philosophique, je trouve quand même que tu as une drôle de conception de la liberté pour vouloir imposer les LL.
Les arguments que tu sors sur MS me semblent d'ailleurs transposables à toi et les LL: Pour ce qui est des prescripteurs, tu souhaites -voire exige- d'avoir des Mozilla sur tous les postes (salle infos) pour je ne sais quels outils de développement, tu veux de la base de donnée MySql/PostgresQL pour telle appli, sans compter l'adorateur de Linus/RMS/... qui est perdu sans OpenOffice.org etc.
Mais les universités utilisent des logiciels libres depuis des lustres. À commencer par gcc, emacs et vim. On trouve aussi beaucoup OpenOffice.org pour les cours de bureautique. Et caml bien sûr, et mozilla. De toute façon, les universités manquent tellement de fric qu'elles ont pas le choix.
Quant à la recherche, elle n'a rien à voir avec tel ou tel logiciel. Ce qui importe c'est le fondement sous-jacent. Si le gars fait de la recherche sur les méta-modèles UML (pas de chance, le gars), il va utiliser Rose ou Objecteering parce que c'est ce qu'il y a de plus complet pour ce qu'il veut faire. Mais son boulot c'est d'étudier certaines notions de méta-modèles, pas de développer ou bugtracker un logiciel libre essayant de remplacer Rose/Objecteering. Comme tout le monde, il a un objectif et il choisit un outil qui fait ce qu'il veut au moment où il en a besoin pour remplir cet objectif.
J'ajoute que chaque chercheur est responsable individuellement de sa recherche. Il n'y a pas de hiérarchie dans la recherche pour ce qui est -justement- des choix scientifiques. Et c'est heureux.
Pour ce qui est de l'enseignement c'est plus compliqué. Il y a des commissions pédagogiques qui établissent un programme. Mais il n'y a quasiment jamais de choix politique de tel ou tel logiciel. C'est le responsable d'un enseignement, avec les administrateurs, qui décide que tel logiciel sera utilisé. On ne se fait rien dicter par l'université.
Il faut bien comprendre que l'enseignement supérieur a un fonctionnemement extrêmement disparate, hétérogène et libre, ce qui fait à la fois sa force et sa faiblesse.
J'aimerais bien que tu me dises donc quelle université prescrit des licences MS?
L'Europe à dejà dépensée plusieurs centaines de milliards d' en licences Microsoft! Alors qu'elle dispose d'universités à même de participer au développement du Logiciel Libre.
C'est une honte pour ceux qui nous gouvernent de ne pas avoir encore engagé une politique qui participe, qui prône et qui diffuse les logiciels libres !
Certes, mais je ne vois pas ce que viennent faire les universités là-dedans: le boulot des universités c'est (l'enseignement et) la recherche, pas le développement de logiciels "finis", fussent-ils libres.
Pour ma part, j'avais une formation très technique (C/C++/Java/Cobol!/Perl) quand je me suis mis à Caml. Au départ ça a été l'horreur : j'aimais pas la syntaxe, j'avais juste l'impression de manipuler une calculette, j'avais un a priori contre le récursif, etc. Classique quoi!
Et puis bon, j'étais bien obligé de m'y mettre pour les cours...
Et là j'ai découvert l'élégance et la concision de la récursivité (avec une syntaxe adaptée bien sûr), un système de types statique très expressif et par inférence (ça c'est magique), l'ordre supérieur, le filtrage, la séparation entre monde fonctionnel et monde impératif...
Et puis ensuite, passage à Ocaml avec ses objets bien plus intéressants qu'en Java et son système de modules (plutôt) évolué.
Et là, on se demande comment on va encore pouvoir programmer dans les autres langages "old school". :-)
De fait la syntaxe est très adaptée au style de programmation "applicatif".
Pour ce qui est de l'efficacité, je suis toujours effaré de voir beaucoup d'informaticiens (notamment les hackers) tout ramener systématiquement à la rapidité et aux capacités d'optimisation. Faut-il que les sempiternels cours de génie logiciel mettant en avant l'abstraction, la réutilisabilité, l'orthogonalité, la maintenabilité, etc, n'aient eu aucune influence sur les étudiants!
Oui oui je connais bien Erlang et ses applications. Aucun doute sur le fait qu'il a fait ses preuves au niveau industriel dans des applis critiques. C'est un très bon langage. La gestion des threads me laisse froid mais le mécanisme de gestion des erreurs et la reconfiguration dynamique sont réellement intéressants.
Mais par contre, l'argument d'Ericsson selon lequel il y a peu d'erreurs liées au typage me fait bien rire.
Les programmeurs habitués à des systèmes de types évolués (comme celui d'OCaml) savent bien qu'un programme refusé à cause d'une erreur de type est généralement (ce n'est pas une loi mathématique mais une constatation) incorrect sur le plan conceptuel. Autrement dit, une erreur dans un programme Erlang, comme dans tout langage, serait une erreur de type pour un système évolué. Bon évidemment, je ne dis pas qu'on peut tout capturer, on sait bien que c'est impossible. Mais le système de types de Caml rattrape un nombre d'erreurs phénoménal.
D'ailleurs des gens ont proposé des systèmes pour Erlang, notamment par inférence (cf travaux de Dagnat). Tout n'est pas réglé, mais ça risque pas de l'être si on ne fait pas de recherche dans cette direction.
C'étaient pas des hackers C à la base. Caml est une création de Guy Cousineau, inspiré du métalangage ML de LCF et créé par Robin Milner.
Xavier Leroy a tout repris à zéro pour sa thèse et a créé (pas tout seul bien sûr) plein de versions de Caml (Light, Special, Objective). Il se trouve qu'en plus d'être un excellent théoricien c'est aussi un putain de programmeur. Il a d'ailleurs développé les threads pour faire tourner Caml...
Je ne suis pas sûr que l'implémentation soit libre au sens de la GPL. Il me semble que tu n'as pas le droit de diffuser une version modifiée des sources, mais uniquement des patchs. C'est assez libre pour moi, mais sûrement pas pour RMS.
Sinon, tu connais beaucoup de langages de programmation qui ne sont pas formels, toi? La spécificité de Caml, c'est qu'on connaît (grosso modo) sa sémantique formelle, ce qui est différent. D'ailleurs, on la connaît à moitié. Je mets au défi quiconque de me sortir toutes les règles de sémantique (abstraite, opérationnelle, voire dénotationelle) et les preuves formelles associées (Church-Rosser, autoréduction, etc) de Caml tel qu'il est implémenté.
Je connais pas de langage ne pouvant pas utiliser des bibliothèques C pour ma part. OK c'est plus ou moins difficile selon les implémentations. Et justement, c'est pas non plus ultra-facile en Caml, malheureusement.
C'est vrai que les foncteurs (modules paramétrés) c'est génial mais c'est pas une invention de Caml non plus. D'ailleurs, il reste pour l'instant quelques limitations gênantes sur lesquels ils travaillent, au demeurant, avec notamment des recherches sur l'intégration des mixins (le monde est petit: ces derniers sont plus ou moins dus à Gilad Bracha qui fait partie maintenant de l'équipe de développement pour Java).
Ces précisions faites, je suis tout à fait d'accord pour encourager à l'utilisation de Caml. Je ne vois personnellement pas de meilleur langage pour l'instant. Pourquoi est-ce le meilleur? Parce que l'équipe Caml est pragmatique et pas jusqu'au-boutiste. Ils veulent une sémantique claire et élégante mais aussi un langage réellement utilisable (un tant soit peu efficace, avec une stratégie d'évaluation "intuitive", etc). Comparé à Haskell, il est certes moins élégant sur le plan théorique, mais c'est un très bon compromis pour ce qu'on attend d'un langage sur les plans théorique et pratique.
Effectivement, ce langage est très expressif mais y'a quand même un problème avec le système de types : les arguments covariants sont possibles (grâce à 'like'). Il est notoire que c'est dangereux. Les travaux de http://www.di.ens.fr/~castagna/(...) résolvent la situation mais c'est évidemment trop tard pour modifier Eiffel.
Sur le fond je pense que nous sommes plutôt d'accord. Voici quand même quelques remarques.
a) ça fait des années que B est utilisé en milieu industriel
c) ça fait maintenant des années que METEOR tourne
N'en rajoute pas tout de même, ce n'est pas encore la consécration. Il y a eu un développement marquant (le système de freinage de METEOR) mais pas grand-chose depuis.
b) ça fait des années que Coq est «prometteur»
Rappelons tout de même que la théorie axiomatique des ensembles date de 1910-1920 alors que la théorie des types a réellement débuté en 1971 (Martin-Löf). Il reste beaucoup de choses à construire, d'autant plus que la théorie des types est plus complexe que la théorie des ensembles (notamment à cause du manque d'extensionnalité).
J'ajoute que B est lui aussi encore en développement: B événementiel, mais aussi définitions inductives (un des derniers dadas d'Abrial) de structures complexes (au lieu d'en rester à certains types de données prédéfinis), etc.
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition.
Je ne crois pas avoir écrit cela mais : «y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.» D'un point de vue formel, spécifier un problème de maths ou plus orienté systèmes, c'est pas vraiment différent.
Elles déterminent des domaines d'applications qui ne sont pas perméables. B a été conçu *pour* ce type de problèmes, ce n'est pas le cas pour Coq.
Effectivement, B est orienté systèmes, surtout avec son procédé de raffinement jusqu'au B0. Et Coq est généraliste dans l'absolu, même si les développements marquants sont en maths formelles. On a quand même les types coïnductifs et l'extraction de code, de même que l'annotation de programmes impératifs (à la Floyd-Hoare et... B).
C'est déjà le cas pour B
Là je ne suis pas d'accord: même pour B ce n'est pas le cas. Le système de freinage de METEOR fait environ 60.000 lignes d'Ada (Abrial dixit) si mes souvenirs sont bons. On est loin d'un programme industriel de plusieurs millions de lignes.
http://savannah.nongnu.org/projects/brillant/(...(...))
Les outils en cours de développement sont en Java mais aussi (surtout) en ... OCaml !! ;-) Par exemple, un prouveur expérimental dénommé BPhox est en cours de réalisation. Il utilise Phox une sorte de version allégée de ... Coq
C'est rigolo mais parmi les participants, je connais un chargé de recherche (collègue de bureau) qui utilisait Coq pour prouver du B parce que l'Atelier B n'est pas assez puissant!
Quant à PhoX, ce n'est pas un Coq light. C'est un assistant fondé sur la logique classique d'ordre supérieur (implémentée en AF2), pas du tout sur le calcul des constructions inductives, qui est en plus intuitionniste. Cela dit, PhoX est vraiment très agréable à utiliser et très «pragmatique».
«Réelles» ça veut dire quoi? Sur des applications industrielles?
Il ne s'agit pas ici de polémiquer, mais bien de poser cette question d'un point de vue scientifique: y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.
D'un point de vue formel, un problème d'ordonnancement (par exemple) ou un problème de maths, c'est kif-kif: c'est juste une chaîne de caractère (dotée d'une sémantique), qui est censée représenter ton problème, et sur laquelle tu effectues un certain nombre de preuves de propriétés.
L'équipe de logique de Nijmegen a ainsi formalisé et certifié en Coq le théorème de d'Alembert-Gauss, ce qui n'est pas plus simple que des problèmes industriels de petite taille.
Et c'est là qu'on peut dire par contre, qu'un problème industriel a la fâcheuse manie d'être de très grande taille, sans être forcément compliqué, d'un point de vue intuitif.
Un gros challenge pour les méthodes formelles consiste donc certainement à un saut «in the large», ce qui est très difficile pour des raisons techniques (explosion du graphe d'états). L'automatisation croissante des outils formels va dans le bon sens, mais il y a encore beaucoup de boulot.
Ce qui fait l'intérêt de la recherche: on va pas reprocher à l'équipe Coq de faire des recherches, c'est son boulot et il y a matière à recherche!
[^] # Re: Hors Sujet [était Re: bijection : définition]
Posté par Anaximandre . En réponse à la dépêche Sortie de Gnome 2.8. Évalué à 2.
Tout l'inverse du bouquin amphigourique d'Hofstadter qui se concentre sur les aspects mécaniques de la numération de Gödel qui, je le répète, ne présente aucun intérêt. Le résultat de Gödel, ce n'est certainement pas qu'on peut représenter des lettres par des nombres ; ça c'est juste un artifice technique connu (c'est même comme ça que fonctionne un ordinateur, tiens tiens). L'approche d'Hofstadter, c'est un peu comme celui qui prétendait lire les grands événements du monde par des analyses de la valeur des lettres hébraïques dans le tanakh.
L'important, c'est la distinction entre démontrabilité et vérité, la diagonalisation, l'existence d'indécidables, l'absence ontologique de métalangage, les conséquences pour les maths et l'info...
[^] # Re: Hors Sujet [était Re: bijection : définition]
Posté par Anaximandre . En réponse à la dépêche Sortie de Gnome 2.8. Évalué à 2.
Beaucoup plus simple à lire, et nettement plus correct d'un point de vue scientifique : le théorème de Gödel, par Nagel, Newmann, Gödel (article original) et Girard, au Seuil (coll. Points Science) : http://www.amazon.fr/exec/obidos/ASIN/2020327783/qid=1095408867/ref(...)
De Girard, on pourra d'ailleurs lire http://iml.univ-mrs.fr/~girard/wtls.ps.gz(...) qui en une dizaine de pages donne une bonne intro à toute la problématique sous-jacente.
[^] # Re: bijection : définition
Posté par Anaximandre . En réponse à la dépêche Sortie de Gnome 2.8. Évalué à 1.
Ça se voit très bien en prenant la contraposée de ton raisonnement qui serait :
x = y => f(x) = f(y)
ce qui est le moins qu'on puisse attendre d'une application !
[^] # Re: bijection : définition
Posté par Anaximandre . En réponse à la dépêche Sortie de Gnome 2.8. Évalué à 4.
f : A --> B est
- injective si pour tous x, y dans A, x <> y => f(x) <> f(y)
càd : des éléments différents ont une image différente.
- surjective si pour tout y dans B, il existe x dans A tel que y = f(x)
càd : f "recouvre" B. On résume ça par f(A) = B.
Le nombre de solutions/antécédents est une conséquence de ces définition et du fait que f est une application.
[^] # Re: Coup d'épée dans l'eau
Posté par Anaximandre . En réponse à la dépêche Est-ce que le logiciel doit prendre en otage les données ?. Évalué à 2.
[^] # Re: Coup d'épée dans l'eau
Posté par Anaximandre . En réponse à la dépêche Est-ce que le logiciel doit prendre en otage les données ?. Évalué à 3.
[^] # Re: Dans le même genre
Posté par Anaximandre . En réponse à la dépêche Râleurs pessimistes ou visionnaires d'un avenir sombre ?. Évalué à -1.
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 1.
Cf mailing-list Caml pour plein de posts à ce sujet.
Ça n'empêche pas qu'il est possible d'effectuer la compilation mais le code obtenu est d'une efficacité moyenne.
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 2.
En l'occurrence, les MV pour Java et C# ne sont pas adaptées à la compilation des langages fonctionnels. Contrairement à ce que tu prétends, il ne s'agit pas juste de compiler vers du code itératif. Pour les langages fonctionnels, on utilise en général certaines techniques pour lesquelles on ne trouve pas de primitive adéquate dans les MV sus-citées, on est donc obligé de passer par des fonctions qui bouffent du temps CPU pour rien. La gestion de la mémoire dynamique est en particulier problématique. Y'a qu'à voir les difficultés pour compiler du OCaml ou du F# vers la MV C#.
Encore une fois je ne critique pas ces MV en tant que telles, je dis juste qu'elles ne constituent pas la solution "universelle".
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 1.
Je travaille grosso modo dans le domaine des langages de programmation et c'est donc un sujet qui m'intéresse. J'expose mon avis et mes doutes sur la question de la réflexivité, au sens large, comme paradigme (parmi d'autres) de programmation.
Tout à fait d'accord sur le fait que la réflexivité est plus facile à implémenter sur un interprète mais ça n'empêche que ça n'a pas de rapport avec le haut niveau supposé du langage.
Pareil pour l'indépendance par rapport au matériel. Rien n'interdit de développer une librairie abstrayant l'OS et de conserver le langage compilé. Évidemment, ça demande du travail mais c'est pas extrêmement compliqué.
Mais dans les deux cas, tout ça c'est le problème des concepteurs de l'environnement d'exécution et on peut se poser la question de leur qualité s'ils développent un interprète uniquement parce que c'est dur de faire un compilo et que c'est plus direct pour l'indépendance par rapport au mtériel. Je crains que ça ne soit souvent le cas de pas mal de langages interprétés de la communauté du libre.
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 1.
Y'a quand même un problème : cette machine virtuelle, comme la JVM, et comme toute MV, a été développée avec certaines fonctionnalités en tête. En l'occurrence, elle a été prévue pour être la cible d'un langage à objets. Par contre, elle n'est pas adaptée à l'exécution des langages fonctionnels.
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 4.
Donc, pour vous (/toi), un langage de haut niveau, ce serait un langage faiblement typé ou réflexif, par exemple?
Dans ce cas, on n'a pas du tout la même conception du haut niveau. Pour moi, un langage de haut niveau, c'est un langage qui a (au moins) les aspects suivants:
- syntaxe et sémantique opérationnelle claires et simples
- système de types fort et expressif
- abstraction importante par rapport à la machine.
La réflexivité entre-t-elle dans ce cadre? La question me semble mal posée (cf. (*) plus bas).
Ceci dit, la réflexivité ne fait pas forcément mauvais ménage avec un typage fort, contrairement à ce qu'on peut lire ici ou là. C'est vrai qu'on a intuitivement du mal à croire qu'on puisse les marier mais en fait, si (cf MetaOCaml, ou les langages à n niveaux).
Par ailleurs, l'implémentation du typage et de l'exécution sont fortement découplées en général, ou alors il y a un problème dans le langage.
J'admets par contre que c'est plus facile d'implémenter la réflexivité dans un interprète, vu qu'on programme ce dernier dans un langage gérant la mémoire à plus haut niveau que le microprocesseur.
(*) La réflexivité est un thème qui réapparaît souvent quand on parle des langages de programmation, et on dit souvent que c'est une fonctionnalité nécessaire. Ce qui m'étonne dans ce discours, c'est que la réflexivité n'est qu'une technique, qu'un moyen. Mais il est vrai que c'est assez fascinant, ce qui à mon avis occulte la réflexion (!) qu'il faut entreprendre.
La discussion ne devrait pas porter sur la réflexivité elle-même mais sur l'objectif auquel elle est censée répondre. Ce but, laissé souvent implicite, c'est en général la reconfiguration dynamique d'un programme, qui implique la génération et le chargement dynamiques de code. Or pour ça on n'a pas nécessairement besoin en pratique de toute la réflexivité.
Utiliser la réflexivité ex abrupto façon Lisp ou même Java, ça revient à contourner le typage (en passant par des quotes ou des chaînes de caractères).
Par contre, si on se concentre sur l'idée de reconfiguration dynamique, on peut trouver des primitives cloisonnées (contrairement à la réflexivité) qui suffisent à produire 99% des programmes (facilement 99% du temps) et qui bénéficient, elles, d'une sémantique abstraite (typage) claire et expressive.
Dans ces conditions, on a le beurre (la reconfiguration dynamique) et l'argent du beurre (la sûreté assurée par le typage fort).
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 1.
[^] # Re: Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn
Posté par Anaximandre . En réponse à la dépêche Mozilla souhaite s'allier à d'autres projet Libres pour faire face à MS-Longhorn. Évalué à 1.
Quel rapport entre l'interprété et le haut-niveau?
[^] # Re: Effectivement...
Posté par Anaximandre . En réponse à la dépêche Le Brésil fait des économies grâce à Linux. Évalué à 2.
Ensuite, permets-moi de te dire que la recherche, l'enseignement et l'administration des moyens (de l'enseignement et de la recherche) prennent suffisamment de temps pour en plus se taper un boulot de développement.
Historiquement, l'INRIA (à l'époque IRIA) a été fondé par De Gaulle pour assurer l'indépendance informatique de la France. Puis sa mission a évolué vers l'informatique plus fondamentale où il est maintenant au top niveau.
Si on estime que le LL est important dans un projet de société, alors ce serait à mon avis plutôt à l'Union Européenne de financer des centres de développement idoines. Mais ce n'est pas le boulot des chercheurs.
Pour ma part, je n'utilise que les LL pour des raisons éthiques (mon côté gauchiste), qualitatives (les LL aboutis sont souvent supérieurs sur le plan technique) et financières (je n'utilise que des LL gratuits, ça me coûte moins cher dans mon travail et ma vie personnelle).
Maintenant, sur le plan philosophique, je trouve quand même que tu as une drôle de conception de la liberté pour vouloir imposer les LL.
Les arguments que tu sors sur MS me semblent d'ailleurs transposables à toi et les LL:
Pour ce qui est des prescripteurs, tu souhaites -voire exige- d'avoir des Mozilla sur tous les postes (salle infos) pour je ne sais quels outils de développement, tu veux de la base de donnée MySql/PostgresQL pour telle appli, sans compter l'adorateur de Linus/RMS/... qui est perdu sans OpenOffice.org etc.
[^] # Re: La France et l'Europe c'est pour quand ?
Posté par Anaximandre . En réponse à la dépêche Le Brésil fait des économies grâce à Linux. Évalué à 1.
Mais les universités utilisent des logiciels libres depuis des lustres. À commencer par gcc, emacs et vim. On trouve aussi beaucoup OpenOffice.org pour les cours de bureautique. Et caml bien sûr, et mozilla. De toute façon, les universités manquent tellement de fric qu'elles ont pas le choix.
Quant à la recherche, elle n'a rien à voir avec tel ou tel logiciel. Ce qui importe c'est le fondement sous-jacent. Si le gars fait de la recherche sur les méta-modèles UML (pas de chance, le gars), il va utiliser Rose ou Objecteering parce que c'est ce qu'il y a de plus complet pour ce qu'il veut faire. Mais son boulot c'est d'étudier certaines notions de méta-modèles, pas de développer ou bugtracker un logiciel libre essayant de remplacer Rose/Objecteering. Comme tout le monde, il a un objectif et il choisit un outil qui fait ce qu'il veut au moment où il en a besoin pour remplir cet objectif.
J'ajoute que chaque chercheur est responsable individuellement de sa recherche. Il n'y a pas de hiérarchie dans la recherche pour ce qui est -justement- des choix scientifiques. Et c'est heureux.
Pour ce qui est de l'enseignement c'est plus compliqué. Il y a des commissions pédagogiques qui établissent un programme. Mais il n'y a quasiment jamais de choix politique de tel ou tel logiciel. C'est le responsable d'un enseignement, avec les administrateurs, qui décide que tel logiciel sera utilisé. On ne se fait rien dicter par l'université.
Il faut bien comprendre que l'enseignement supérieur a un fonctionnemement extrêmement disparate, hétérogène et libre, ce qui fait à la fois sa force et sa faiblesse.
J'aimerais bien que tu me dises donc quelle université prescrit des licences MS?
[^] # Re: Et la France et l'Europe c'est pour quand ?
Posté par Anaximandre . En réponse à la dépêche Le Brésil fait des économies grâce à Linux. Évalué à -1.
C'est une honte pour ceux qui nous gouvernent de ne pas avoir encore engagé une politique qui participe, qui prône et qui diffuse les logiciels libres !
Certes, mais je ne vois pas ce que viennent faire les universités là-dedans: le boulot des universités c'est (l'enseignement et) la recherche, pas le développement de logiciels "finis", fussent-ils libres.
[^] # Re: On oublie toujours OCaml
Posté par Anaximandre . En réponse à la dépêche Havoc Pennington se pose des questions sur les langages du libre. Évalué à 1.
Et puis bon, j'étais bien obligé de m'y mettre pour les cours...
Et là j'ai découvert l'élégance et la concision de la récursivité (avec une syntaxe adaptée bien sûr), un système de types statique très expressif et par inférence (ça c'est magique), l'ordre supérieur, le filtrage, la séparation entre monde fonctionnel et monde impératif...
Et puis ensuite, passage à Ocaml avec ses objets bien plus intéressants qu'en Java et son système de modules (plutôt) évolué.
Et là, on se demande comment on va encore pouvoir programmer dans les autres langages "old school". :-)
De fait la syntaxe est très adaptée au style de programmation "applicatif".
Pour ce qui est de l'efficacité, je suis toujours effaré de voir beaucoup d'informaticiens (notamment les hackers) tout ramener systématiquement à la rapidité et aux capacités d'optimisation. Faut-il que les sempiternels cours de génie logiciel mettant en avant l'abstraction, la réutilisabilité, l'orthogonalité, la maintenabilité, etc, n'aient eu aucune influence sur les étudiants!
[^] # Re: Erlang a également été oublié
Posté par Anaximandre . En réponse à la dépêche Havoc Pennington se pose des questions sur les langages du libre. Évalué à 3.
Mais par contre, l'argument d'Ericsson selon lequel il y a peu d'erreurs liées au typage me fait bien rire.
Les programmeurs habitués à des systèmes de types évolués (comme celui d'OCaml) savent bien qu'un programme refusé à cause d'une erreur de type est généralement (ce n'est pas une loi mathématique mais une constatation) incorrect sur le plan conceptuel. Autrement dit, une erreur dans un programme Erlang, comme dans tout langage, serait une erreur de type pour un système évolué. Bon évidemment, je ne dis pas qu'on peut tout capturer, on sait bien que c'est impossible. Mais le système de types de Caml rattrape un nombre d'erreurs phénoménal.
D'ailleurs des gens ont proposé des systèmes pour Erlang, notamment par inférence (cf travaux de Dagnat). Tout n'est pas réglé, mais ça risque pas de l'être si on ne fait pas de recherche dans cette direction.
[^] # Re: On oublie toujours OCaml
Posté par Anaximandre . En réponse à la dépêche Havoc Pennington se pose des questions sur les langages du libre. Évalué à 5.
Xavier Leroy a tout repris à zéro pour sa thèse et a créé (pas tout seul bien sûr) plein de versions de Caml (Light, Special, Objective). Il se trouve qu'en plus d'être un excellent théoricien c'est aussi un putain de programmeur. Il a d'ailleurs développé les threads pour faire tourner Caml...
Je ne suis pas sûr que l'implémentation soit libre au sens de la GPL. Il me semble que tu n'as pas le droit de diffuser une version modifiée des sources, mais uniquement des patchs. C'est assez libre pour moi, mais sûrement pas pour RMS.
Sinon, tu connais beaucoup de langages de programmation qui ne sont pas formels, toi? La spécificité de Caml, c'est qu'on connaît (grosso modo) sa sémantique formelle, ce qui est différent. D'ailleurs, on la connaît à moitié. Je mets au défi quiconque de me sortir toutes les règles de sémantique (abstraite, opérationnelle, voire dénotationelle) et les preuves formelles associées (Church-Rosser, autoréduction, etc) de Caml tel qu'il est implémenté.
Je connais pas de langage ne pouvant pas utiliser des bibliothèques C pour ma part. OK c'est plus ou moins difficile selon les implémentations. Et justement, c'est pas non plus ultra-facile en Caml, malheureusement.
C'est vrai que les foncteurs (modules paramétrés) c'est génial mais c'est pas une invention de Caml non plus. D'ailleurs, il reste pour l'instant quelques limitations gênantes sur lesquels ils travaillent, au demeurant, avec notamment des recherches sur l'intégration des mixins (le monde est petit: ces derniers sont plus ou moins dus à Gilad Bracha qui fait partie maintenant de l'équipe de développement pour Java).
Ces précisions faites, je suis tout à fait d'accord pour encourager à l'utilisation de Caml. Je ne vois personnellement pas de meilleur langage pour l'instant. Pourquoi est-ce le meilleur? Parce que l'équipe Caml est pragmatique et pas jusqu'au-boutiste. Ils veulent une sémantique claire et élégante mais aussi un langage réellement utilisable (un tant soit peu efficace, avec une stratégie d'évaluation "intuitive", etc). Comparé à Haskell, il est certes moins élégant sur le plan théorique, mais c'est un très bon compromis pour ce qu'on attend d'un langage sur les plans théorique et pratique.
[^] # Re: Erlang a également été oublié
Posté par Anaximandre . En réponse à la dépêche Havoc Pennington se pose des questions sur les langages du libre. Évalué à 1.
[^] # Re: On oublie toujours OCaml
Posté par Anaximandre . En réponse à la dépêche Havoc Pennington se pose des questions sur les langages du libre. Évalué à 0.
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par Anaximandre . En réponse à la dépêche Après X, voici Y.... Évalué à 0.
a) ça fait des années que B est utilisé en milieu industriel
c) ça fait maintenant des années que METEOR tourne
N'en rajoute pas tout de même, ce n'est pas encore la consécration. Il y a eu un développement marquant (le système de freinage de METEOR) mais pas grand-chose depuis.
b) ça fait des années que Coq est «prometteur»
Rappelons tout de même que la théorie axiomatique des ensembles date de 1910-1920 alors que la théorie des types a réellement débuté en 1971 (Martin-Löf). Il reste beaucoup de choses à construire, d'autant plus que la théorie des types est plus complexe que la théorie des ensembles (notamment à cause du manque d'extensionnalité).
J'ajoute que B est lui aussi encore en développement: B événementiel, mais aussi définitions inductives (un des derniers dadas d'Abrial) de structures complexes (au lieu d'en rester à certains types de données prédéfinis), etc.
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition.
Je ne crois pas avoir écrit cela mais : «y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.» D'un point de vue formel, spécifier un problème de maths ou plus orienté systèmes, c'est pas vraiment différent.
Elles déterminent des domaines d'applications qui ne sont pas perméables. B a été conçu *pour* ce type de problèmes, ce n'est pas le cas pour Coq.
Effectivement, B est orienté systèmes, surtout avec son procédé de raffinement jusqu'au B0. Et Coq est généraliste dans l'absolu, même si les développements marquants sont en maths formelles. On a quand même les types coïnductifs et l'extraction de code, de même que l'annotation de programmes impératifs (à la Floyd-Hoare et... B).
C'est déjà le cas pour B
Là je ne suis pas d'accord: même pour B ce n'est pas le cas. Le système de freinage de METEOR fait environ 60.000 lignes d'Ada (Abrial dixit) si mes souvenirs sont bons. On est loin d'un programme industriel de plusieurs millions de lignes.
http://savannah.nongnu.org/projects/brillant/(...(...))
Les outils en cours de développement sont en Java mais aussi (surtout) en ... OCaml !! ;-) Par exemple, un prouveur expérimental dénommé BPhox est en cours de réalisation. Il utilise Phox une sorte de version allégée de ... Coq
C'est rigolo mais parmi les participants, je connais un chargé de recherche (collègue de bureau) qui utilisait Coq pour prouver du B parce que l'Atelier B n'est pas assez puissant!
Quant à PhoX, ce n'est pas un Coq light. C'est un assistant fondé sur la logique classique d'ordre supérieur (implémentée en AF2), pas du tout sur le calcul des constructions inductives, qui est en plus intuitionniste. Cela dit, PhoX est vraiment très agréable à utiliser et très «pragmatique».
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par Anaximandre . En réponse à la dépêche Après X, voici Y.... Évalué à 1.
Il ne s'agit pas ici de polémiquer, mais bien de poser cette question d'un point de vue scientifique: y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.
D'un point de vue formel, un problème d'ordonnancement (par exemple) ou un problème de maths, c'est kif-kif: c'est juste une chaîne de caractère (dotée d'une sémantique), qui est censée représenter ton problème, et sur laquelle tu effectues un certain nombre de preuves de propriétés.
L'équipe de logique de Nijmegen a ainsi formalisé et certifié en Coq le théorème de d'Alembert-Gauss, ce qui n'est pas plus simple que des problèmes industriels de petite taille.
Et c'est là qu'on peut dire par contre, qu'un problème industriel a la fâcheuse manie d'être de très grande taille, sans être forcément compliqué, d'un point de vue intuitif.
Un gros challenge pour les méthodes formelles consiste donc certainement à un saut «in the large», ce qui est très difficile pour des raisons techniques (explosion du graphe d'états). L'automatisation croissante des outils formels va dans le bon sens, mais il y a encore beaucoup de boulot.
Ce qui fait l'intérêt de la recherche: on va pas reprocher à l'équipe Coq de faire des recherches, c'est son boulot et il y a matière à recherche!
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par Anaximandre . En réponse à la dépêche Après X, voici Y.... Évalué à 1.