Moi je ne trouve pas cela choquant, parce que c'est une validation formelle qui a été faite :
> The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.
C'est de la validation formelle, c'est à dire prouvée mathématiquement. Mais attention, ca ne prouve pas qu'il n'y a pas de bugs ou que le code est parfait, ca prouve simplement que le code du noyau répond aux spécifications formelles établies par ses concepteurs.
Vulgairement ca veut dire que les mecs sont sûrs que ce qu'ils ont codé répond exhaustivement (et uniquement) aux besoins. La validation formelle (et pas uniquement de code source) est un domaine certes pas nouveau mais pas encore très répandu. Surtout parce qu'il ne serait pas rentable dans tous les domaines. Vu le temps nécessaire à valider formellement un modèle, et le fait qu'il ne fasse "que" dire "OK, je retrouve toutes tes specs formelles dans ton modèle/ton code", c'est plus de l'utilité des mecs qui conçoivent des moteurs d'avion ou des satellites que pour le logiciel de retouche photo de ma maman...
Le code source de la vérification doit exister quelque part mais ne donnera pas plus de valeur à cette validation. La validation en elle-même est suffisante puisqu'elle mettra des liens entre le code source et les exigences des specs, point.
"Je ne suis pas d’accord avec ce que vous dites, mais je me battrai jusqu’au bout pour que vous puissiez le dire." (cette phrase n'est pas de moi, mais d'un grand homme, je te laisse chercher)
Alors si tu fais référence à Voltaire, je dis "FAUX", cette phrase lui a été attribuée à tort (lien).
Je ne m'étendrai pas dans le fond du débat parce que vous vous exprimez mieux que moi mais je voulais souligner cette erreur trop souvent lue un peu partout.
PS: Einstein n'a pas non plus donné son avis sur la corrélation entre la fin des abeilles et de l'homme.
PPS: Malraux n'a non plus jamais parlé ou écrit à propos de l'éventuelle spiritualité du XXIe siècle corrélée à son existence.
14.04 ? ca nous laisse le temps de le voir venir. On n'est jamais qu'à la 11.10, s'ils suivent leur process de numérotation de version actuel alors ca veut dire qu'on aura un téléphone sous Ubuntu en 2014...
Bon en même temps c'est peut-être plus crédible comme ca...
c'est une des grosses raisons que j'ai quasi tout en libre, sauf l'OS, sur mon desktop
Je comprends pas cette phrase. Tu as tout en libre, sauf l'OS de ton desktop ?
C'est à dire que tu as acheté ou fabriqué du matériel libre et que tu as installé un OS proprio dessus ? oO
Ici, au Québec, je n'ai pas le droit non plus parce que la France est également considérée comme à risque à cause de la vache folle dans les années 90...
On pourrait aller plus loin et avant de proposer une nouvelle gestion du temps sous UNIX, on pourrait carrément réfléchir à une nouvelle définition du temps.
Anéfé, la physique est en train de nous montrer que la vitesse de la lumière peut être dépassée. Or la vitesse de la lumière est (était) une constante que l'on associait à la durée de 9 192 631 770 périodes de la radiation correspondant à la transition entre les niveaux hyperfins F=3 et F=4 de l’état fondamental S½^6 de l’atome de césium 133 (Seconde_(temps)). ces deux constantes permettaient de définir le mètre dans la mesure où distance=vitesse*temps.
Si, dans cet état de fait, les constantes commencent à devenir des variables, tout fout l'camp moi j'vous dis ! Alors UTC ou pas UTC...
Pour ceux qui ont installé leur propre webmail/groupware, quel à été votre choix et pourquoi ?
Moi en fait, je n'ai pas fait un choix mais plusieurs, selon les besoins et les terminaux.
Je loue un serveur dédié sur lequel j'ai mes mails en Imap et quand je ne suis pas connecté avec un Thunderbird j'ai le choix :
- Horde, ils viennent de passer à la version 4 comme dit plus haut: plus lourd mais de loin le webmail le plus complet avec son calendrier et son carnet d'adresses.
- Roundcube, je l'ai utilisé pendant un moment puis plus trop ensuite, mais pour une raison qui m'échappe, un beau jour il s'est mis à ne plus marcher (connexion impossible) et j'ai pas cherché plus loin. Cela dit, c'est un bon webmail 2.0 rapide.
- IlohaMail, le meilleur dans sa catégorie webmail light, efficace et utilisable sur un intelligent téléphone. Mais depuis la mise à jour Debian 6.0, il n'a plus voulu marcher non plus...
- Squirrelmail, installé, testé mais j'ai jamais été convaincu par son interface que je trouve moche et pas adaptée aux petits écrans (netbook notamment)
et y'en a eu plein d'autres...
Maintenant je suis sur Horde 4 mais je vais retenter roundcube pour voir. Il sera sûrement plus rapide.
Je proteste sur l'interprétation que tu as faite sur cette actualité !
La physique n'est pas fausse, il y a simplement une opportunité, si cette expérience de vitesse supérieure à c se confirme, que notre compréhension de l'univers s'étende au delà de ce qu'on connait jusqu'à présent.
En d'autres termes, peut-être que dans un certain temps nous ne dirons plus "la réponse à la question universelle sur la vie, l'univers et le reste est 42", mais, "la réponse à la question sur le référentiel de l'univers limité à l'espace-temps einsteinien, la probabilité de l'existence de la vie dans ce même référentiel, et le reste des particules et quantas limités aux 4 dimensions est, avec une probabilité non-nulle, 42"
Toute personne proposant 43 doit argumenter sa réponse et la replacer dans son contexte, en tenant compte bien évidemment des conditions initiales, des résultats attendus et de l'imprécision des instruments de mesure.
Moi ca fait des années que ce genre d'aventures me gratte mais quelles sont les options pour les "vieux" (à peine plus de 30 ans) en pleine santé, sans avoir à s'engager dans l'armée ?
Elle est suspendue sur quels cours l'action Apple ? Si c'est sur le marché américain c'est normal, c'est parce que Wall Street est fermé et ouvrira demain matin (demain 15h pour la France).
Sinon ben c'est un sujet de troll supplémentaire qui s'en va. Avec Bill Gates à la retraite, le couple maudit des années 80/90 dans l'informatique personnelle n'est plus. J'ai l'impression que personne d'aussi charismatique ne s'est encore imposé dans ce milieu...
Tiens, je connaissais pas ceux-là. Effectivement, ils proposent aussi de l'illimité à 5Mb/s, comme un peu tous les FAI illimités en ADSL...
Le mieux (ou moins pire) que j'ai vu c'est Youmano qui propose sur le cable du 8Mb illimité ou sur l'ADSL du 5Mb illimité. Le choix va être cornélien :(
Pas de bridage mais une Segmentation en fonction des débits/volume de donnée
Comme au Canada avec ISP Rogers
Mmmmmmmm, moi qui vient d'arriver au Québec et qui s'arrache les cheveux à trouver un FAI qui me convienne je ne peux qu'approuver.
La situation dans la belle province est la suivante, deux gros fournisseurs de tuyaux se partagent le marché de l'Internet: Bell avec les lignes téléphoniques cuivre et Videotron avec le réseau câblé. Bien que l'un fasse aussi de la télé par câble et l'autre fasse aussi de l'ADSL mais bon. Les deux ont en place un bridage de la consommation et avec eux l'écrasante majorité des autres FAI. Seuls quelques petits proposent encore de l'illimité mais sans garantie que ca durera éternellement, et avec des débits au mieux de 5Mb. Ajoutez à cela un prix qu'un français moyen jugerait excessif (en général les québécois payent une centaine de dollars, ~70€ (sans les taxes)) pour leur abonnement triple-play et vous obtenez un bon casse-tête pour ma pomme...
ca dépend de ce que tu entends par comparer.
Si comparer signifie calquer bêtement tous les indicateurs islandais sur les français, non.
Si comparer signifie examiner et s'inspirer des changements socio, économiques, législatifs, constitutionnels, etc. Alors oui parce qu'à l'inverse on ne peut rien comparer avec rien:
- La France et l'Allemagne : pas la même croissance, pas la même politique...
- La France et la Grèce : pas la même taille, pas les mêmes problèmes...
- La France et les USA : pas la même philosophie, pas les mêmes contraintes...
- la France et Mars : pas la même population, pas la même distance au soleil...
et ainsi de suite
Ah ben niveau matériel ils font des souris quand même, donc c'est bonnet blanc...
Blague à part, on peut comparer Google à Microsoft, voire IBM qui en son temps a eu les mêmes accusations mais comme toujours ce n'est pas la même chose. A mon avis, au moins au début, le coté matos de Google ne sera pas leur vitrine mais plutôt un bonus qui leur permettra d'améliorer et de booster leur R&D dans cette branche, leur cœur de métier restera pendant encore un moment les services web avec le moteur de recherche, les mails, etc.
Par contre ils se positionnent clairement dans le secteur qui va croître progressivement, jusqu'à dépasser puis annihiler l'informatique personnelle dans un futur accessible (si on en croit les Cassandres du métier). De la même manière que Microsoft s'est marié à Nokia. Peut-être bien qu'on verra apparaître d'autres mariages entre des gros constructeurs et des gros fournisseurs de services et logiciels. Qui sait, un petit smartphone Samsung/Oracle peut sortir des cartons un jour ?
Quoi qu'il en soit, Google/Moto c'est pas pire que le reste, tant qu'on a de la concurrence et du choix moi je m'en tamponne...
[^] # Re: Question
Posté par Babelouest (site web personnel) . En réponse à la dépêche Petites brèves sur les distributions. Évalué à 10.
Équipe recherche et innovation chez certaines multinationales
[^] # Re: Monde de merde
Posté par Babelouest (site web personnel) . En réponse au journal linuxfr en baisse de forme, heureusement numerama est là. Évalué à 1.
Fallait pas lancer le dist-upgrade...
[^] # Re: Avis de Linus Torvalds sur les micro-noyaux
Posté par Babelouest (site web personnel) . En réponse à la dépêche Entretien avec Andrew Tanenbaum à propos de MINIX. Évalué à 3.
Moi je ne trouve pas cela choquant, parce que c'est une validation formelle qui a été faite :
> The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.
C'est de la validation formelle, c'est à dire prouvée mathématiquement. Mais attention, ca ne prouve pas qu'il n'y a pas de bugs ou que le code est parfait, ca prouve simplement que le code du noyau répond aux spécifications formelles établies par ses concepteurs.
Vulgairement ca veut dire que les mecs sont sûrs que ce qu'ils ont codé répond exhaustivement (et uniquement) aux besoins. La validation formelle (et pas uniquement de code source) est un domaine certes pas nouveau mais pas encore très répandu. Surtout parce qu'il ne serait pas rentable dans tous les domaines. Vu le temps nécessaire à valider formellement un modèle, et le fait qu'il ne fasse "que" dire "OK, je retrouve toutes tes specs formelles dans ton modèle/ton code", c'est plus de l'utilité des mecs qui conçoivent des moteurs d'avion ou des satellites que pour le logiciel de retouche photo de ma maman...
Le code source de la vérification doit exister quelque part mais ne donnera pas plus de valeur à cette validation. La validation en elle-même est suffisante puisqu'elle mettra des liens entre le code source et les exigences des specs, point.
[^] # Re: war inside my head
Posté par Babelouest (site web personnel) . En réponse au journal CCC au pape. Évalué à 2.
Alors si tu fais référence à Voltaire, je dis "FAUX", cette phrase lui a été attribuée à tort (lien).
Je ne m'étendrai pas dans le fond du débat parce que vous vous exprimez mieux que moi mais je voulais souligner cette erreur trop souvent lue un peu partout.
PS: Einstein n'a pas non plus donné son avis sur la corrélation entre la fin des abeilles et de l'homme.
PPS: Malraux n'a non plus jamais parlé ou écrit à propos de l'éventuelle spiritualité du XXIe siècle corrélée à son existence.
PPPS: etc.
# Ouh la belle
Posté par Babelouest (site web personnel) . En réponse à la dépêche Canonical va lancer un OS mobile pour téléphones et tablettes. Évalué à 3.
14.04 ? ca nous laisse le temps de le voir venir. On n'est jamais qu'à la 11.10, s'ils suivent leur process de numérotation de version actuel alors ca veut dire qu'on aura un téléphone sous Ubuntu en 2014...
Bon en même temps c'est peut-être plus crédible comme ca...
[^] # Re: Bravo
Posté par Babelouest (site web personnel) . En réponse au journal Barnes & Noble résiste à M$. Évalué à 2.
Rejoins-nous dans le Maemo-N900-OpenMoko club !
[^] # Re: Interview de Linus Torvalds sur mukware.com
Posté par Babelouest (site web personnel) . En réponse au journal Linux 3.2 en route. Évalué à 2.
c'est une des grosses raisons que j'ai quasi tout en libre, sauf l'OS, sur mon desktop
Je comprends pas cette phrase. Tu as tout en libre, sauf l'OS de ton desktop ?
C'est à dire que tu as acheté ou fabriqué du matériel libre et que tu as installé un OS proprio dessus ? oO
[^] # Re: Moi je veux bien donner, mais ...
Posté par Babelouest (site web personnel) . En réponse au journal Don de soi. Évalué à 2.
Ici, au Québec, je n'ai pas le droit non plus parce que la France est également considérée comme à risque à cause de la vache folle dans les années 90...
[^] # Re: Defective by design
Posté par Babelouest (site web personnel) . En réponse à la dépêche Une plainte d’un éditeur autour de l’astrologie menace la base de données tz / zoneinfo. Évalué à 5.
On pourrait aller plus loin et avant de proposer une nouvelle gestion du temps sous UNIX, on pourrait carrément réfléchir à une nouvelle définition du temps.
Anéfé, la physique est en train de nous montrer que la vitesse de la lumière peut être dépassée. Or la vitesse de la lumière est (était) une constante que l'on associait à la durée de 9 192 631 770 périodes de la radiation correspondant à la transition entre les niveaux hyperfins F=3 et F=4 de l’état fondamental S½^6 de l’atome de césium 133 (Seconde_(temps)). ces deux constantes permettaient de définir le mètre dans la mesure où distance=vitesse*temps.
Si, dans cet état de fait, les constantes commencent à devenir des variables, tout fout l'camp moi j'vous dis ! Alors UTC ou pas UTC...
[^] # Re: Et telnet alors ?
Posté par Babelouest (site web personnel) . En réponse au sondage Quel est votre client de courriel / webmail ?. Évalué à 1.
(ou un truc approchant, je me souviens plus de la syntaxe exacte, elle est dans un script shell obscurcit...)
[^] # Re: De quel Linux on parle au juste ?
Posté par Babelouest (site web personnel) . En réponse au journal Loi/lobby contre offre/consommation. Évalué à 9.
Qu'elle soit stable ou cynique ?
(je suis déjà dehors...)
[^] # Re: Qt ?
Posté par Babelouest (site web personnel) . En réponse à la dépêche Meego est mort ! Vive Tizen !. Évalué à 4.
La vitesse à laquelle de nouveaux terminaux/OS/Frameworks sortent chaque jour...
[^] # Re: choix Webmail / GroupWare
Posté par Babelouest (site web personnel) . En réponse à la dépêche Roundcube webmail 0.6 est disponible. Évalué à 2.
Pour ceux qui ont installé leur propre webmail/groupware, quel à été votre choix et pourquoi ?
Moi en fait, je n'ai pas fait un choix mais plusieurs, selon les besoins et les terminaux.
Je loue un serveur dédié sur lequel j'ai mes mails en Imap et quand je ne suis pas connecté avec un Thunderbird j'ai le choix :
- Horde, ils viennent de passer à la version 4 comme dit plus haut: plus lourd mais de loin le webmail le plus complet avec son calendrier et son carnet d'adresses.
- Roundcube, je l'ai utilisé pendant un moment puis plus trop ensuite, mais pour une raison qui m'échappe, un beau jour il s'est mis à ne plus marcher (connexion impossible) et j'ai pas cherché plus loin. Cela dit, c'est un bon webmail 2.0 rapide.
- IlohaMail, le meilleur dans sa catégorie webmail light, efficace et utilisable sur un intelligent téléphone. Mais depuis la mise à jour Debian 6.0, il n'a plus voulu marcher non plus...
- Squirrelmail, installé, testé mais j'ai jamais été convaincu par son interface que je trouve moche et pas adaptée aux petits écrans (netbook notamment)
et y'en a eu plein d'autres...
Maintenant je suis sur Horde 4 mais je vais retenter roundcube pour voir. Il sera sûrement plus rapide.
[^] # Re: tout façon tout ce que vous dites est faux puisque la physique est fause
Posté par Babelouest (site web personnel) . En réponse au journal Réponse, Univers, Ça, 42.... Évalué à 1.
Je proteste sur l'interprétation que tu as faite sur cette actualité !
La physique n'est pas fausse, il y a simplement une opportunité, si cette expérience de vitesse supérieure à c se confirme, que notre compréhension de l'univers s'étende au delà de ce qu'on connait jusqu'à présent.
En d'autres termes, peut-être que dans un certain temps nous ne dirons plus "la réponse à la question universelle sur la vie, l'univers et le reste est 42", mais, "la réponse à la question sur le référentiel de l'univers limité à l'espace-temps einsteinien, la probabilité de l'existence de la vie dans ce même référentiel, et le reste des particules et quantas limités aux 4 dimensions est, avec une probabilité non-nulle, 42"
Toute personne proposant 43 doit argumenter sa réponse et la replacer dans son contexte, en tenant compte bien évidemment des conditions initiales, des résultats attendus et de l'imprécision des instruments de mesure.
[^] # Re: hummmmm dit-il en rêvant
Posté par Babelouest (site web personnel) . En réponse au journal photos libre d'Antarctique. Évalué à 4.
OK, merci des infos !
[^] # Re: hummmmm dit-il en rêvant
Posté par Babelouest (site web personnel) . En réponse au journal photos libre d'Antarctique. Évalué à 1.
Moi ca fait des années que ce genre d'aventures me gratte mais quelles sont les options pour les "vieux" (à peine plus de 30 ans) en pleine santé, sans avoir à s'engager dans l'armée ?
[^] # Re: Ça dépend des fenêtres
Posté par Babelouest (site web personnel) . En réponse au sondage L'écran de mon ordinateur est orienté. Évalué à 1.
Have you tried turning it off and on again? (The IT Crowd inside)
Sinon si ca ne marche toujours pas, c'est que le problème doit être quantique. As-tu essayé de t'éloigner de ton accélérateur de particules ?
[^] # Re: la vraie mauvaise nouvelle ne devrait pas tarder
Posté par Babelouest (site web personnel) . En réponse au journal Coup de tonnerre à Cupertino. Évalué à 1.
Elle est suspendue sur quels cours l'action Apple ? Si c'est sur le marché américain c'est normal, c'est parce que Wall Street est fermé et ouvrira demain matin (demain 15h pour la France).
Sinon ben c'est un sujet de troll supplémentaire qui s'en va. Avec Bill Gates à la retraite, le couple maudit des années 80/90 dans l'informatique personnelle n'est plus. J'ai l'impression que personne d'aussi charismatique ne s'est encore imposé dans ce milieu...
[^] # Re: Mais non !
Posté par Babelouest (site web personnel) . En réponse au journal Horreur, enfer et damnation: Fin de l'illimité. Évalué à 2.
Tiens, je connaissais pas ceux-là. Effectivement, ils proposent aussi de l'illimité à 5Mb/s, comme un peu tous les FAI illimités en ADSL...
Le mieux (ou moins pire) que j'ai vu c'est Youmano qui propose sur le cable du 8Mb illimité ou sur l'ADSL du 5Mb illimité. Le choix va être cornélien :(
[^] # Re: Mais non !
Posté par Babelouest (site web personnel) . En réponse au journal Horreur, enfer et damnation: Fin de l'illimité. Évalué à 1.
Pas de bridage mais une Segmentation en fonction des débits/volume de donnée
Comme au Canada avec ISP Rogers
Mmmmmmmm, moi qui vient d'arriver au Québec et qui s'arrache les cheveux à trouver un FAI qui me convienne je ne peux qu'approuver.
La situation dans la belle province est la suivante, deux gros fournisseurs de tuyaux se partagent le marché de l'Internet: Bell avec les lignes téléphoniques cuivre et Videotron avec le réseau câblé. Bien que l'un fasse aussi de la télé par câble et l'autre fasse aussi de l'ADSL mais bon. Les deux ont en place un bridage de la consommation et avec eux l'écrasante majorité des autres FAI. Seuls quelques petits proposent encore de l'illimité mais sans garantie que ca durera éternellement, et avec des débits au mieux de 5Mb. Ajoutez à cela un prix qu'un français moyen jugerait excessif (en général les québécois payent une centaine de dollars, ~70€ (sans les taxes)) pour leur abonnement triple-play et vous obtenez un bon casse-tête pour ma pomme...
[^] # Re: Gouverner, c'est prévoir. Limiter internet, c'est régresser.
Posté par Babelouest (site web personnel) . En réponse au journal Horreur, enfer et damnation: Fin de l'illimité. Évalué à 2.
ca dépend de ce que tu entends par comparer.
Si comparer signifie calquer bêtement tous les indicateurs islandais sur les français, non.
Si comparer signifie examiner et s'inspirer des changements socio, économiques, législatifs, constitutionnels, etc. Alors oui parce qu'à l'inverse on ne peut rien comparer avec rien:
- La France et l'Allemagne : pas la même croissance, pas la même politique...
- La France et la Grèce : pas la même taille, pas les mêmes problèmes...
- La France et les USA : pas la même philosophie, pas les mêmes contraintes...
- la France et Mars : pas la même population, pas la même distance au soleil...
et ainsi de suite
[^] # Re: Je ne sais pas trop qu'en penser
Posté par Babelouest (site web personnel) . En réponse au journal Google rachète motorola. Évalué à 3.
Ah ben niveau matériel ils font des souris quand même, donc c'est bonnet blanc...
Blague à part, on peut comparer Google à Microsoft, voire IBM qui en son temps a eu les mêmes accusations mais comme toujours ce n'est pas la même chose. A mon avis, au moins au début, le coté matos de Google ne sera pas leur vitrine mais plutôt un bonus qui leur permettra d'améliorer et de booster leur R&D dans cette branche, leur cœur de métier restera pendant encore un moment les services web avec le moteur de recherche, les mails, etc.
Par contre ils se positionnent clairement dans le secteur qui va croître progressivement, jusqu'à dépasser puis annihiler l'informatique personnelle dans un futur accessible (si on en croit les Cassandres du métier). De la même manière que Microsoft s'est marié à Nokia. Peut-être bien qu'on verra apparaître d'autres mariages entre des gros constructeurs et des gros fournisseurs de services et logiciels. Qui sait, un petit smartphone Samsung/Oracle peut sortir des cartons un jour ?
Quoi qu'il en soit, Google/Moto c'est pas pire que le reste, tant qu'on a de la concurrence et du choix moi je m'en tamponne...
[^] # Re: 640k is enougth
Posté par Babelouest (site web personnel) . En réponse au journal Trente ans. Évalué à 1.
Ca aurait dû être suffisant pour tout le monde ne tout cas...
[^] # Re: Presque partout
Posté par Babelouest (site web personnel) . En réponse au journal https everywhere. Évalué à 8.
Des noms ! Des noms !
[^] # Re: intello
Posté par Babelouest (site web personnel) . En réponse au journal Nom de geek pour une chatte ?. Évalué à 2.
Ou alors "bruit des croquettes quand tu agites la boite".