auve a écrit 310 commentaires

  • [^] # Re: Le cerveau n'est pas logique

    Posté par  . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.

    SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne > comporte pas d’ambigüité. Et le compilo est certifié.

    Tout ce que tu dis est vrai (et pour cause !), je préciserais simplement que "ne pas comporter d'ambigüité" veut dire qu'on peut donner au langage une sémantique formelle claire. Ça va aussi avec un certain nombre d'articles de recherche présentant le langage et diverses techniques de compilation de façon très propre. Un compilateur prouvé correct en Coq pour une version très antérieure de SCADE, Lustre, a d'ailleurs été récemment présenté à la conférence PLDI.

  • [^] # Re: Le cerveau n'est pas logique

    Posté par  . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 6.

    Il y a un rapport entre why3 et coq ?

    Why3 est ce qu'on appelle un générateur de conditions de vérification, c'est à dire un outil transformant un programme contenant des spécifications formelles (typiquement formulées sous la forme de pré- et post-conditions) en un ensemble de formules logiques (les dites conditions de vérification) dont la validité implique que le programme respecte sa spécification. Une fois générées, Why3 transmet ces conditions de vérification à divers outils pour essayer de démontrer leur validité automatiquement; celles pour lesquelles ce processus échoue sont traduites vers Coq pour permettre la preuve manuelle.

    (Par ailleurs, l'auteur principal de Why3 est aussi un des contributeurs historiques au cœur de Coq.)

  • [^] # Re: go 2.0

    Posté par  . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.

    […] est-ce que les chercheurs en programmation (financés par l'argent public, etc.) devraient avoir comme finalité dans la vie d'aider l'industrie à écrire du code crade et jetable plus vite qu'avant ? […] Et rendre les programmeurs jetables/interchangeables en uniformisant les outils et techniques (une autre chose dont les managers dans l'industrie auraient bien envie), on devrait travailler dessus aussi ?

    Je pense que c'est plus ou moins explicitement l'objectif d'une large partie de la recherche en ingénierie logicielle qui a lieu en France et à l'étranger.

  • # Choix du langage

    Posté par  . En réponse au journal Simple Provisioning System. Évalué à 5.

    Salut,

    C'est chouette de partager ton code avec d'autre dans l'espoir qu'il soit utile. Merci !

    Petite question : pourquoi avoir choisi C++ pour un programme qui consiste essentiellement à manipuler des chaînes de caractères puis à les passer au shell ? Il me semble que ce n'est pas connu pour être une des grandes forces du langage.

  • # Bingo

    Posté par  . En réponse au journal [ANN] Channel IRC Sur le Domain Driven Design #dddfr. Évalué à 10.

    Domain Driven Design […] Command Query Responsability Segregation […] Event Sourcing, Event Store […] Clean, hexagonales, Layer […]

    FOUTAISES !

  • [^] # Re: Et si on prenait ça comme un retour?

    Posté par  . En réponse au journal Word vs TeX. Évalué à 3.

    Ça serait bien que la solution WYSIWYM du XXIe siècle vienne du libre, parce que si ça n'est pas le cas, on ne pourra pas résister très longtemps, ne serait-ce que pour une simple raison de productivité.

    On m'a dit du bien de Patoline. Ils refont à la fois le langage d'entrée, histoire d'avoir quelque-chose de plus raisonnable et moderne que TeX et LaTeX, et le moteur de rendu lui-même. Je ne sais pas trop ce que ca vaut, ne l'ayant pas utilisé moi-même.

  • [^] # Re: La géométrie algébrique et le reste...

    Posté par  . En réponse au journal Alexandre Grothendieck est bronsonisé. Évalué à 4.

    Uniquement de son vivant, vu qu'il voulait que tout soit détruit à sa mort.

    Je ne crois pas que cela ait été son intention, à en croire la lettre trouvable sur http://www.grothendieckcircle.org et reproduite dans le billet de David Madore cité plus haut :

    Toute édition ou diffusion de tels textes qui aurait été faits par le passé sans mon accord, ou qui serait faite à l'avenir et de mon vivant, à l'encontre de ma volonté expresse précisée ici, est illicite à mes yeux.

  • [^] # Re: Plutôt beauté du design

    Posté par  . En réponse au journal "beauté du code". Évalué à 5.

    Tu sais que tu parles de John Carmack, un des meilleurs codeurs de tous les temps ?

    Tout le monde aimerait que ce soit vrai mais c'est une légende urbaine. John Carmack n'a pas écrit cette fonction.

  • [^] # Re: TV

    Posté par  . En réponse au journal Un billet de réflexion sur l'échec de Linux sur le Desktop. Évalué à 10.

    Venant du concepteur historique de C++, c'est vraiment la paille de l'hôpital qui se fout de la poutre de la charité…

  • [^] # Re: En pratique

    Posté par  . En réponse à la dépêche Le chiffrement homomorphe. Évalué à 2.

    Je cite l'article :

    Oui mais voilà, dans la pratique, cela donne des clés gigantesques (plusieurs méga-octets, alors qu'une clé RSA ne pèse qu'entre 128 et 512 octets), et les calculs (addition et multiplications) peuvent être jusqu'à 1000x plus lents que les opérations non-homomorphes.

  • [^] # Re: Modestie...

    Posté par  . En réponse à la dépêche Un entretien avec Lennart Poettering. Évalué à 3.

    Steve Jobs t'a fait quelque-chose quand tu étais petit ? Sûrement la même chose que Bill Gates à Albert_.

  • # Je vais donc aussi...

    Posté par  . En réponse au journal Fermez les écoutilles. Évalué à 10.

    ... arrêter de lire les journaux de DLFP.

  • [^] # Re: Un dernier petit pas pour C++0x

    Posté par  . En réponse à la dépêche La version 4.6 du compilateur GCC est disponible. Évalué à 1.

    Parce que le hardware est comme ça, et que spécifier la sémantique d'un programme contenant des data-races de façon portable et sans inhiber les optimisations faisables par le compilateur est quasiment impossible à l'heure actuelle ?

    http://rsim.cs.illinois.edu/Pubs/10-cacm-memory-models.pdf

  • [^] # Re: Pas besoin de MS

    Posté par  . En réponse au journal Où l'on parle de Microsoft et des méthodes démocratiques de Ben Ali.... Évalué à 1.

    Et ce certificat de certification a été automatiquement accepté comme légitime par ton navigateur (i.e. les certificats "finaux" signés par celui-ci sont acceptés), simplement parce qu'il existe un chemin de confiance entre lui et un certificat racine, où cela a réclamé une procédure supplémentaire ?

  • [^] # Re: Pas besoin de MS

    Posté par  . En réponse au journal Où l'on parle de Microsoft et des méthodes démocratiques de Ben Ali.... Évalué à -2.

    Et si elle signe un certificat de certification pour un gouvernement ?

    Hum, je crois que le fonctionnement de l'infrastructure à clé publique t'échappe complètement. Les certificats racines ne peuvent pas servir à en créer de nouveaux qui seraient automatiquement acceptés par ton navigateur. Encore heureux !

  • # On peut rire de tout...

    Posté par  . En réponse au journal [Breaking News] Impacts du tremblement de terre sur DLFP. Évalué à -10.

    ... ou pas.

  • [^] # Re: Glissement de la source ?

    Posté par  . En réponse au journal Symbian, Moblin/Meego et Android sont dans bateau nommé Nokia. Évalué à 4.

    Pourquoi bouse ? Pourquoi semi-fermée (cf. git plus haut) ?
  • [^] # Re: Critique sans avoir essayé

    Posté par  . En réponse au journal gnome3.org. Évalué à 3.

    Sorti des applis du dock, j'ai juste compris qu'on devais se farcir le finder et le répertoire Applications, ou tout est en vrac. Tout sauf utilisable.

    Euh un macounet ayant besoin de plus de cinq applications fera ctrl - espace pour afficher Spotlight (le service de recherche d'OSX), tapera une partie du nom de l'appli qu'il veut lancer, et appuiera sur entrée...
  • [^] # Re: Oui mais non

    Posté par  . En réponse au journal Un portable 15.6" sous GNU/Linux à prix plancher !. Évalué à 0.

    Dans les 15'6 (je ne sais pas si tu les comptes comme des 15 pouces), y a quand même un paquet de portables avec écrans dits "1080p"... Regarde chez Sony (Vaio) ou Dell (XPS L510x et assimilés). Les Vaio doivent probablement t'offrir de bonnes résolutions en 13'.

    Sinon, le MacBook Air 13' a une résolution de 1440x900.
  • [^] # Re: Il faut résonner en terme de Toolkit et non en tant que DE

    Posté par  . En réponse au journal Qt dans Ubuntu. Évalué à 7.

    Je pense que ça résonne effectivement beaucoup dans le crâne de Mark S.
  • [^] # Re: J'attends désespérément un moteur de production potable...

    Posté par  . En réponse à la dépêche Redo, un remplaçant de choix pour Make. Évalué à 1.

    Il ne confond pas du tout, et OMake n'est absolument pas une solution fournissant un patron de Makefile, mais bien un système de build autonome.
  • [^] # Re: make ?

    Posté par  . En réponse à la dépêche Redo, un remplaçant de choix pour Make. Évalué à 3.

    Je l'ai fais de tête c'est un oublie simple à prendre en compte.

    Euh, si tu ajoutes une version correcte de la fonctionnalité demandée par Bruno (dépendance vers les headers utilisés par un .c) à un Makefile aussi simple, ça devient de loin la partie la plus compliquée...
  • [^] # Re: L'hypocrisie d'Apple

    Posté par  . En réponse au journal [BreakingNews] VLC retiré de l'iOS AppStore !. Évalué à 4.

    La procédure qui coûte 99 euros par an ?
  • [^] # Re: Jabber HS hier soir

    Posté par  . En réponse au journal Skype HS hier soir. Évalué à 2.

    N'empêche, si deux mecs motivés arrivent à faire ça, je me pose la question de 10 mecs payés pour faire de l'espionnage industriel par exemple...

    Euh certes, mais ta phrase peut laisser penser que les gens en question étaient de gentils gus dans leur garage qui ont fait ça un dimanche après-midi, alors qu'en pratique ils sont/étaient chercheurs en sécurité informatique chez EADS et en ont largement chié d'après mes souvenirs. À mon avis ils rentrent pour une large mesure dans la case « payés à faire de l'espionnage industriel » !
  • [^] # Re: Non, mais perso ....

    Posté par  . En réponse au journal C++ a été créé pour augmenter le salaire des programmeurs. Évalué à 1.

    Parole de Lead Architect ?