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

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

  Posté par kadreg (page perso, ) le 20/11/2006 à 13:23. (lien). É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 Antoine Reilles (Jabber id, page perso, ) le 20/11/2006 à 13:54. (lien). Évalué à 2.

    scheme aussi, avec des compilos comme bigloo
    http://www-sop.inria.fr/mimosa/fp/Bigloo/
    qui peut aussi tourner sur un runtime .net

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

  Posté par Sylvain Briole (page perso, ) le 20/11/2006 à 14:26. (lien). É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 TImaniac (page perso, ) le 20/11/2006 à 14:52. (lien). É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/

    --
    MonoFrance

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

      Posté par Sylvain Briole (page perso, ) le 20/11/2006 à 15:23. (lien). É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 TImaniac (page perso, ) le 20/11/2006 à 16:26. (lien). É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.

        --
        MonoFrance

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

      Posté par Thomas Douillard () le 20/11/2006 à 19:53. (lien). É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 MrLapinot (Jabber id, page perso, ) le 20/11/2006 à 20:49. (lien). É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.

        --
        Mr Lapinot - Electrons prisonniers (blog)

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

          Posté par Thomas Douillard () le 20/11/2006 à 21:08. (lien). É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 lambada () le 20/11/2006 à 22:06. (lien). É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 Thomas Douillard () le 21/11/2006 à 09:40. (lien). É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 totof2000 () le 21/11/2006 à 16:28. (lien). Évalué à 1.

                Autant pour moi,
                C'est "au temps pour moi".

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

                  Posté par Thomas Douillard () le 21/11/2006 à 16:48. (lien). Évalué à 4.

                  C'est un sujet de troll récurent, hop un petit lien :
                  
                  http://www.langue-fr.net/index/A/au_temps-autant.htm
                  
                  Donc voilà, personne n'étant capable de vraiment trancher, ce qui alimente le troll, j'ai décidé perso d'écrire la forme que j'ai toujours pensée valide avant de tomber sur le premier troll sur le net, et que j'ai toujours comprise intuitivement comme indiqué dans le lien ("c'est autant pour moi")
                  
                  Et si t'es pas content je te merde :p
                  (D'ailleurs c'est beaucoup plus drôle de laisser vivre le troll)

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

              Posté par iug () le 21/11/2006 à 14:49. (lien). É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 Thomas Douillard () le 21/11/2006 à 15:05. (lien). É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 lambada () le 21/11/2006 à 18:21. (lien). É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

• [^]Re: Réponses manquantes

  Posté par lambada () le 20/11/2006 à 13:22. (lien). Évalué à 7.

  Roooh et [ ] Pierre Tramo ? C'est le sondage ou jamais !

[X] : Victoire !

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

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

  Posté par hophophop () le 20/11/2006 à 15:40. (lien). É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 Farvardin (page perso, ) le 20/11/2006 à 15:46. (lien). É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 ?

    --
    Tous ensemble contre l'esclavitude des logiciels privateurs !

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

      Posté par hophophop () le 20/11/2006 à 15:55. (lien). É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 Farvardin (page perso, ) le 20/11/2006 à 16:26. (lien). É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 ?

        --
        Tous ensemble contre l'esclavitude des logiciels privateurs !

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

          Posté par hophophop () le 20/11/2006 à 16:31. (lien). Évalué à 2.

          ben ils la telechargeront pas chez sun si sun veut pas la fournir a une ip iranienne, c'est ce que je voulais dire.
          
          Ca n'exclue pas que des tiers la fournissent aux messants iraniens.
          
          Cela dit, je ne sais pas si ces clauses d'export sont une obligation legale americaine ou un choix de ces boites de ne pas exporter vers ces pays...
          (je vote pour la premiere option, a confirmer par quelqu'un qui sait de quoi il parle, ie pas moi)

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

            Posté par Mathieu Stumpf (Jabber id, page perso, ) le 21/11/2006 à 08:49. (lien). Évalué à 2.

            http://pages.cafr.ebay.ca/help/policies/embargo.html
            
            En résumé c'est donc bien des lois aux US qui force cette politique. M'enfin c'est connu, ne serait-ce que le coups pour cuba...

            --
            Le wiki de l'association culture libre : collection d'œuvres sous licence art libre.

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

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

  Posté par taratatatata () le 20/11/2006 à 21:06. (lien). É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

• [^]Re: Trop tard

  Posté par Cali_Mero () le 21/11/2006 à 04:49. (lien). É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 !

  --
  #define MAGIC 0xdefaced /* I should've patented this number -cliph */