Journal Sondage Java sous GPL, donnez votre avis à Sun

Posté par  (site web personnel) .
Étiquettes : aucune
0
20
nov.
2006
Comme dit dans la nouvelle sur LinuxFr.org, Sun a diffusé la machine virtuelle Hotspot, le compilateur Java, et le système d’aide Javahelp sous GPL :
http://linuxfr.org/2006/11/13/21624.html

Sur le site http://www.java.net/ Sun vous demande votre avis :

Quel est votre opinion sur le choix de la GPL comme licence Java open source ?
[ ] : C'est exactement ce que j'espérais
[ ] : J'aurais préféré une autre licence, mais je suis content
[ ] : J'aurais préféré un autre licence, et je suis mécontent
[ ] : Je ne pense pas que qu'il aurait dû être open source du tout

C'est peut-être utile de leur donner votre avis ?

  • # [X] : C'est exactement ce que j'espérais

    Posté par  . Évalué à 7.

    Au vu des derniers évènements concernant ce genre de plateforme, c'était vraiment la meilleure chose à faire, la meilleure réponse à donner. Bravo les gens de chez Sun ! Java est très loin d'être mon langage préféré, mais on peut rêver que le bytecode devienne adressable avec d'autres langages.

    • [^] # Re: [X] : C'est exactement ce que j'espérais

      Posté par  . Évalué à 4.

      > on peut rêver que le bytecode devienne adressable avec d'autres langages.

      C'était déjà la cas. Les specifications de la JVM étant publiques, de nombreux langages sont capab les de sortir sous forme de bytecode java. Ada, eifel, python, C# ...

      http://www.robert-tolksdorf.de/vmlanguages.html

    • [^] # Re: [X] : C'est exactement ce que j'espérais

      Posté par  (site web personnel) . Évalué à 2.

      Avec cette libération, je m'intéresse maintenant à cette plateforme jusque là relativement inconnue.

      Y-a-t'il quelque part un banc-d'essai qui a été réalisé pour valider la qualité (dans le sens fiabilité) de la/des machine(s) virtuelle(s)?
      Sont-elles stables? Ou sont-elles aussi sujettes à bugs, comme certains processeurs bien physiques?
      Je ne m'y connais que peu en théorie des langages, mais peut-être que quelque part il y aurait moyen de prouver la qualité de la machine/l'exactitude de la machine?

      Sinon, après un survol rapide : le C semble être absent. Impossible à compiler et faire tourner sur ce genre de machine? Faut-il impérativement un langage orienté objet à la base?

      • [^] # Re: [X] : C'est exactement ce que j'espérais

        Posté par  (site web personnel) . Évalué à 2.

        je m'intéresse maintenant à cette plateforme jusque là relativement inconnue.
        C'est une plateforme très très connue en milieu professionnel.

        Sont-elles stables? Ou sont-elles aussi sujettes à bugs, comme certains processeurs bien physiques?
        Aucun soft n'est parfait, mais la VM de Sun est bien entendu stable (depuis le temps qu'elle existe elle peut bien :) ) et puis c'est plus facile à patcher qu'un processeur physique ;)

        mais peut-être que quelque part il y aurait moyen de prouver la qualité de la machine/l'exactitude de la machine?
        En théorie, oui, en pratique non.

        le C semble être absent. Impossible à compiler et faire tourner sur ce genre de machine?
        La VM de Sun a été conçue pour être utilisée avec le langage Java, orienté objet, c'est donc beaucoup plus naturel d'y intégrer des langages objets. Après on peut très bien s'amuser à faire tourner du C dessus, mais il ne faut pas espérer un niveau d'intégration profond. (exposer des API pour Java toussa). Exemple de compilo C vers JVM : http://www.axiomsol.com/

        • [^] # Re: [X] : C'est exactement ce que j'espérais

          Posté par  (site web personnel) . Évalué à 2.

          >> je m'intéresse maintenant à cette plateforme jusque là relativement inconnue.
          > C'est une plateforme très très connue en milieu professionnel.

          Je me suis mal exprimé : elle m'était relativement inconnue.
          Je travaille dans le développement matériel/logiciel dans le monde embarqué, mais Java et autres JVM n'ont jamais franchi jusqu'à présent les portes de mes applications, pour la simple et bonne raison qu'on cause principalement C (voire parfois C++) chez nous, en raison du passé du code (qui a parfois 15 ans d'âge).

          J'avais raté dans la page le compilo C vers JVM : intéressant en effet.

          J'ai néanmoins du mal à me faire une image précise, dans le cas où je recherche une portabilité "extrème". Aurais-je tendance à privilégier :
          - une solution logicielle à base de C norme ANSI bien propre.
          - ou une solution logicielle à base d'un langage pouvant être compilé en vue d'utilisation sur une JVM.
          Si je me pose cette question, c'est que j'ai rarement vu un processeur ou une plateforme (comprendre processeur + carte mère + système d'exploitation) non livrée avec un compilateur C, alors qu'une JVM m'a rarement été proposée.

          Les JVM stables et éprouvées (je suppose que celle du "constructeur", à savoir Sun est la première la catégorie), sont elles facilement portables sur un nouveau processeur si le constructeur met à disposition un compilateur C?

          • [^] # Re: [X] : C'est exactement ce que j'espérais

            Posté par  (site web personnel) . Évalué à 2.

            Les JVM stables et éprouvées (je suppose que celle du "constructeur", à savoir Sun est la première la catégorie), sont elles facilement portables sur un nouveau processeur si le constructeur met à disposition un compilateur C?
            Il existe différentes JVM, dans différentes éditions, notamment pour l'embarqué (plus légères, etc.). Evidemment, si la JVM est portable, c'est avant tout parcqu'il y a dessous un compilateur C pour la compiler :)
            Enfin si tu veux mon avis, l'intérêt de la JVM c'est d'être portable pour Java, pas d'être portable pour du C. Donc soit t'utilise la JVM, et t'en profite pour utiliser un langage de plus "haut niveau", soit tu garde ton appli en C qui est portable, sans cibler de JVM.

        • [^] # Re: [X] : C'est exactement ce que j'espérais

          Posté par  . Évalué à 2.


          mais peut-être que quelque part il y aurait moyen de prouver la qualité de la machine/l'exactitude de la machine?
          En théorie, oui, en pratique non.


          C'est curieux, j'aurais dit l'inverse :) Enfin, un truc du genre: En théorie, non, en pratique, peut être. Pour prouver l'exactitude, on doit tomber à un moment ou à un autre sur le problème de l'arrêt ( http://fr.wikipedia.org/wiki/Probl%C3%A8me_de_l%27arr%C3%AAt ), qui est indécidable dans le cas général. En pratique, peut être que la JVM est théoriquement prouvable ? C'est pas parce que le prblème est indécidable dans le cas général qu'il l'est pas dans le cas particulier de la JVM. Bon, j'en doute, la JVM étant un morceau de code qui lui même interprête du code, on doit tomber sur de belles merdes théoriques, cf la preuve du problème de l'arrêt

          Bon, après, en pratique, c'est rare qu'on s'amuse à essayer de prouver un programme de cette taille ...

          • [^] # Re: [X] : C'est exactement ce que j'espérais

            Posté par  (site web personnel) . Évalué à 1.

            <warning type="approximations">
            On ne peut pas tout prouver (en particulier, on ne peut prouver aucune propriété non triviale d'une machine de Turing si je ne dis pas de connerie), mais on peut prouver que la machine virtuelle (ou un programme en général) répond bien à certaines spécifications. C'est le domaine de la certification logicielle, ça utilise essentiellement de la logique, et effectivement on a de jolis résultats théoriques parfois un peu galères à mettre en pratique (notamment parce que les démonstrations ne sont que rarement automatiques, en général semi-automatiques).
            </warning>

            Merci de corriger les bêtises.

            • [^] # Re: [X] : C'est exactement ce que j'espérais

              Posté par  . Évalué à 2.

              Effectivement, pour prouver qu'un programme fait bien ce qu'on veut qu'il fasse (la correction) il faut bien commencer par savoir ce qu'on veut qu'il fasse ... Et que la machine le sache aussi. Il faut commencer par écrire les spécifiactions du programme, formellement (en B ou Coq par exemple).

              Un autre problème étant de s'assurer que les specs sont elles mêmes correctes :)

              Sinon pour la preuve semi-automatique, c'est vrai en B par exemple, qui à si je me souviens bien du mal à prouver des propriétés dès qu'on touche à des cardinalités d'ensemble si je me souviens bien, sachant que B est un langage de spec ensembliste. Il faut ajouter des lemmes pour aider le prouveur si besoin.

              Warning aussi, mes connaissances en spec formelles se résument à des cours de B en DUT :)

              • [^] # Re: [X] : C'est exactement ce que j'espérais

                Posté par  . Évalué à 3.

                Je ne connais pas B, mais je sais qu'en Coq, tu écris ta spécification dans un langage particulier, puis la prouves interactivement, avec certaines étapes plus ou moins automatisées à l'aide de "tactiques", plusieurs bibliothèques de ces dernières étant disponibles.

                Une fois la preuve établie (c'est évidemment la partie difficile), Coq est capable d'en extraire un code source en OCaml ou Haskell (via l'isomorphisme de Curry-Howard) qui sera correct par construction (si tant est que le petit coeur "trusted" de Coq, les axiomes, le compilo OCaml, le hardware, l'OS soient eux-mêmes dignes de confiance bien sur).

                Coq ne part pas d'un programme pré-existant pour essayer de prouver sa correction vis à vis des spécifications.

                • [^] # Re: [X] : C'est exactement ce que j'espérais

                  Posté par  . Évalué à 2.

                  Autant pour moi, c'est la même chose pour B : on écrit la spec dans un langage ensembliste "abstrait", puis on raffine vers du code de plus en plus "concret" (comprendre proche d'un langage classique) compilable en C, ADA, et d'autres, en prouvant à chaque étape du raffinage que la spec ne sera pas violée.

                • [^] # Re: [X] : C'est exactement ce que j'espérais

                  Posté par  . Évalué à 0.

                  Encore faudrait-il être confiant dans le fait que le prouveur Coq est plus stable que la JVM... et que la probabilité d'erreur dans les preuves humaines qui se cachent derrière soit plus faible que la probabilité d'erreur dans le code de la JVM. On tombe dans un problème d'oeuf et de poule c'est comique.

                  Etant donné le nombre de personnes qui utilise Coq et le nombre de personnes qui utilisent la JVM, je suis plus que réservé...

                  • [^] # Re: [X] : C'est exactement ce que j'espérais

                    Posté par  . Évalué à 2.

                    Le principe de ces trucs là, c'est de ne prouver "à la main" que vraiment les briques de bases, genre les fonctions vraiment de base.

                    De faire relire ces preuves super simple par pleins de gens, histoire d'être sûrs que ces preuves de bases sont correctes, et de construire l'implémentation en construisant toutes les bibliothèques à partir de ces briques de bases prouvées à la main, et en faisant tout vérifier par le prouveur de manière semi-automatique.

                    Alors certe, c'est un peu chateau de carte, mais c'est bien plus simple d'implémenter et de prouver et tester des briques de bases genre l'insertion d'un élément dans un tableau sans dépassement de capacité que de tester la JVM.

                  • [^] # Re: [X] : C'est exactement ce que j'espérais

                    Posté par  . Évalué à 2.

                    Encore faudrait-il être confiant dans le fait que le prouveur Coq est plus stable que la JVM...


                    Si stable = exempt de bugs ici, alors pour faire confiance à une preuve écrite par Coq tu dois faire confiance au coeur de Coq, relativement petit justement pour éviter les risques (+ le hardware, le compilo et autres cités plus haut mais ça s'applique aussi à la JVM).

                    que la probabilité d'erreur dans les preuves humaines qui se cache derrière soit plus faible que la probabilité d'erreur dans le code de la JVM.


                    Si la preuve passe Coq, elle est garantie sans erreur et le code généré aussi, c'est bien l'intérêt.
                    (bien sur en partant des principes donnés plus haut concernant le coeur de coq, le compilo, la génération de code, la théorie et autres)
                    http://coq.inria.fr/doc/faq.html#htoc7

                    On tombe dans un problème d'oeuf et de poule c'est comique.


                    Le problème c'est qu'on ne puisse pas réécrire Coq en Coq, mais bon ! Sacré Kurt ;-)

                    Etant donné le nombre de personnes qui utilise Coq et le nombre de personnes qui utilisent la JVM, je suis plus que réservé...

                    De toute façon j'apportais juste des précisions sur le fonctionnement de Coq, pas de son applicabilité à l'écriture d'une VM. Xavier Leroy et son équipe semblent s'intéresser à l'écriture d'un compilo prouvé formellement :
                    http://pauillac.inria.fr/~xleroy/compcert-backend/
                    http://pauillac.inria.fr/~xleroy/publi/cfront.pdf
                    http://groups.google.com/group/fa.caml/browse_thread/thread/(...)

  • # Réponses manquantes

    Posté par  (site web personnel, Mastodon) . Évalué à 0.

    [ ] j'en sais rien
    [ ] je me fiche un peu
    [ ] on verra bien
    [ ] 42

    La gelée de coings est une chose à ne pas avaler de travers.

  • # [X] : Victoire !

    Posté par  . Évalué à 2.

    Après s'être tant battu contre cette technologie au départ très verrouillée, c'est le moindre des choix à proposer question satisfaction…

  • # [X] : C'est exactement ce que j'espérais

    Posté par  . Évalué à 2.

    Le meilleur des choix pour un maximum de liberté

    • [^] # Re: [X] : C'est exactement ce que j'espérais

      Posté par  . Évalué à 5.

      c'est beau ce que tu dis, on dirait une pub pour une lessive...

      • [^] # Re: [X] : C'est exactement ce que j'espérais

        Posté par  . Évalué à 5.

        bash 2 en 1 ?


        Sinon, java était auparavant interdit à l'export vers certains pays, comme l'Iran par exemple (le téléchargement était bloqué d'ailleurs lorsque l'ip du téléchargeur venait d'un pays maudis par les USA).

        Est-ce que le passage à la GPL permet de passer outre à cela ? Ou est-ce que d'un point de vue légal il y aura encore quelque chose qui bloquera ?

        Only wimps use tape backup: real men just upload their important stuff on megaupload, and let the rest of the world ~~mirror~~ link to it

        • [^] # Re: [X] : C'est exactement ce que j'espérais

          Posté par  . Évalué à 2.

          Legalement surement rien, pas plus qu'avant (quoique j'ai deja vu ce genre de clauses pour le sdk de brew, une plateforme pour telepone mobile, va savoir avec les ricains)
          Maintenant si sun a decide de ne pas fournir de licence aux iraniens, ils ne fourniront pas de licence aux iraniens. GPL n'implique pas que le distributeur soit oblige de donner une licence a qui la demande.

          • [^] # Re: [X] : C'est exactement ce que j'espérais

            Posté par  . Évalué à 2.

            non, en fait je pensais que du coup le code source étant librement téléchargeable, des iraniens pourront éventuellement le télécharger et le compiler eux-même ?

            Only wimps use tape backup: real men just upload their important stuff on megaupload, and let the rest of the world ~~mirror~~ link to it

  • # [ ] : C'est exactement ce que j'espérais

    Posté par  . Évalué à 2.

    Et ça fera enfin un peu de concurrence à Mono :)
    Plus de choses pourront être implémentées, plus d'apprioris pour ajouter du code Java dans les distribs, que du bon.

    D'ailleurs Mono pourrait également profiter d'améliorations provenant de Java et vis versa. (Je pense à la machine virtuelle)

    • [^] # Re: [ ] : C'est exactement ce que j'espérais

      Posté par  . Évalué à 2.

      "D'ailleurs Mono pourrait également profiter d'améliorations provenant de Java et vis versa. (Je pense à la machine virtuelle)"

      Tu t'avances.
      Novell a besoin des droits sur le code contribué à Mono pour avoir la possibilité de changer la licence du bousin.
      Ils n'intègreront pas la moindre ligne de code en provenance de Java, vu que Sun ne donnera jamais leur copyright/le droit de changer la licence.

      De même, à ce propos, il n'y aura pas la moindre ligne de code de GNU Classpath / GCJ qui pourra aller chez Sun, qui doit garder le contrôle de la bête.

  • # Trop tard

    Posté par  (site web personnel) . Évalué à 3.

    On ne peux plus voter !

    Je ne sais pas combien de temps leur sondage reste en ligne. En tout cas, ils sont passés à u autre sondage ;-( Dommage, il n'y a pas eu beaucoup de votant en tout.

    • [^] # Re: Trop tard

      Posté par  . Évalué à 4.

      Voici tout de même les résultats ( http://today.java.net/pub/pq/132 ), en français et dans l'ordre :


      75,7% (505 Votes) : C'est exactement ce que j'espérais
      12,5% (84 Votes) : J'aurais préféré une autre licence, mais je suis content
      8% (54 Votes) : Je ne pense pas que qu'il aurait dû être open source du tout
      3,5% (24 Votes) : J'aurais préféré un autre licence, et je suis mécontent


      Les plus observateurs remarqueront que 0,3% des votants ont porté leur voix sur Pierre Tramo. Sans doute un vote constestataire !

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.