Matthieu Moy a écrit 3249 commentaires

Sur un azerty, oui ...

> Comment ça les starters pour M****D***O* ne tournent que sous windows ?

C'est bien ça la pratique anticoncurentielle ! Microsoft empêche Jayce de faire une version indépendante d'un autre OS. C'est fou !

Oui, mais c'est la merde a tapper dans mozilla ... la succession de deux < par contre, devrait marcher, mais est bouffée par templeet.

Allez, un view page source plus loin :

- Il apprend, il absorbe ; il devient chaque jour plus intelligent.

- Rassembler des infos est seulement le premier pas vers la sagesse, mais partager des infos est le premier pas vers une communauté.

- Un joueur qui rend une équipe grande a plus de valeur qu'un grand joueur. Se perdre dans le groupe pour le bien du groupe, ça c'est du travail d'équipe.

- Ce qu'il apprend, nous l'apprenons tous. Ce qu'il sais, nous en bénéficions tous.

- Et est-ce qu'il à un nom ?
- Son nom ? Son nom est Linux.

Ca serait cool que les guillements français << comme ça >> marchent, et en particulier, ca serait cool que l'article de la news soit lisible ... ;-)

et socrate est un chat.

Le monsieur, il a dit nombre, pas entiers ;-)

Mais la seule réalité, ce sont les ensembles, d'abord !

On m'aurait menti ! Je suis dans une université littéraire à l'insus de mon plein gré ?

C'est quoi ta définition d'une science ?

Moi, dans le larousse, j'ai entre autres :

Savoir, ensemble de connaissances que l'on acquiert par l'étude, l'expérience, l'observation, etc.

[...]

Les sciences exactes, fondées essentiellement sur le calcul et l'observation (mathématiques, physique, chimie, etc.).


A moins que tu ne fasse partie de ces gens qui sont plus intelligents que les dictionnaires, il y a un truc qui m'échappe ...

Euh, Be n'étais pas obligé d'accepter, je crois ...

Moi, je trouve pas que ce soit une si mauvaise nouvelle :

MS reconnait indirectement ses pratiques anti-concurrentielles, vu que sinon, ils auraient été surs de gagner en cas de procès.

Un peu de sous qui sort de chez MS et qui va chez les concurents. Je dis bien "un peu", parce que la somme reste assez dérisoire à cette échelle ...

Tu peux préciser ?

Les maths non plus ne sont pas une science alors ... ?!?

http://www.google.fr/intl/fr/press/metrics.html(...)

Google a 60% des parts de marché ...
MSN : 7%
Yahoo : 13%

Pour météor, c'est du B en effet. Enfin, le noyau dur est en B, mais il communique avec d'autres modules moins critiques qui n'ont pas été prouvés formellement, ... et qui manifestement plantent de temps en temps :-( Enfin disont que quand tu demande à un spécialiste de la question si météor à déjà planté, il te réponds qu'il n'y a eu aucun plantage qui ne soit pas du à des données erronées envoyées par un module extérieur, et c'est assez lourd de sous-entendus ! Si mes souvenirs sont bons, c'est 500 personnes.mois pour 50 000 lignes de code. (aille aille $$$)

Pour Ariane, je crois que c'est surtout de l'interprétation abstraite qui a été utilisée. Pas assez d'ailleurs :-(

Si le programme est suffisament simple (pas d'allocation dynamique de mémoire, pas d'appels récursifs non bornés, ...), on peut s'en sortir en modélisant le système par un automate, et les techniques de model-checking + interprétation abstraite marchent plutôt bien. Il y a pas mal de code de ce genre dans Airbus par exemple. Dans ce cas, c'est tout automatique, mais les algos sont toujours exponentiels dans le pire cas, donc, des fois, il faut 10^42 années et 10^21 peta octets de RAM pour avoir la réponse, ... L'avantage pour les systèmes matériels, c'est qu'on est toujours dans ce cas là. (t'as déjà vu une puce de silicium faire de l'allocation dynamique de mémoire ?)

Pour des programmes plus complexes, avec structures de données dynamiques, là, il n'y a pas d'algorithme qui puisse prouver le système, et on a même démontré qu'il ne pouvait pas y en avoir (c'est indécidable). Dans ce cas, on peut tenter un peu d'interpétation abstraite (polyspace fait ça par exemple, M$ a un outil comme ça en interne), qui permet de trouver certaines erreurs et de montrer qu'il n'y aura pas d'erreurs à certains endroits, mais il y a toujours des cas ou on ne peut rien dire de façon automatique. Donc, si on veut tout prouver, en effet, il faut tout faire à la main. Au niveau industriel, c'est surtout l'atelier B (ou plutôt une variante au niveau de l'interface -- basé sur Emacs ;-) -- la balbulette) qui domine, mais on peut aussi citer PVS (malheureusement réputé pour être buggé, ce qui est un comble), coq (moins de bac+12, s'abstenir. Il faut déjà pas mal de théorie pour comprendre comment démontrer que 0 != 1 ...), ... Dans tous les cas, les preuves de théorèmes, c'est très long et très chiant. J'ai passé plus d'une journée à prouver un algo de tri de tableau par insertion par exemple (bon, un mec expérimenté ira plus vite, mais y'a pas mal de boulot en tous cas.)

Ce qui est dommage chez free, c'est qu'ils fournissent plein de bon softs libres sur le CD, il mentionnent même le fait que c'est open source.

Mais ça m'est déjà arrivé de tout bien configurer un Netscape chez quelqu'un (un vieux, la machine est pas assez puissante pour un Mozilla), de lui expliquer "quand tu recevra ton kit, il faut mettre ton mot de passe ici". Quelques jours plus tard, la personne utilisait MSIE + OE : "Ben ouais, ça m'a mis ça a la place de Netscape, je sais pas comment changer". (nb : l'icône de NS était toujours sur le bureau ...)

Facile : C'est pour l'année prochaine.

[ Hint : ça fait depuis 91 qu'on peut dire ça chaque année ;-) ]

TeX, et à la mort de D Knuth, la version sera figée à \pi.

A notter que Metafont utilise le même système mais tends vers $e$

Emacs aussi.

1 soft foireux dans Ariane 5 = le milliard ;-)
1 soft foireux dans un Airbus = pas mal non plus je pense ...

Maintenant, c'est clair qu'un bug dans un programme non critique n'est pas très couteux, alors que toutes les puces sont plus ou moins critiques ...

Mais ça ne réponds pas à la question de départ qui était que le vocabulaire des softeux/hardeux impliquait une plus grande rigueur ;-)

[ disclaimer : bossant dans la vérif formelle de soft, il est normal que je m'insurge de tes propos ;-) ]

> Vu que l'info est née après l'électronique,

Ca se discute. Il y avait des modèles de machines de Turing avant que l'élèctronique ne puisse en faire autant je crois.

> D'ailleurs ta dernière phrase montre bien où on trouve le plus de rigueur...

Pas tellement.

Jargon informatique :

Validation = Verifier que le soft est bon
Verification = Verifier formellement que le soft est bon
Test = Verifier par l'execution que le soft est bon

Jargon electronique :

Validation = Verification = Verifier que le design est correct
Test = Verifier que la puce est physiquement bien fabriquée par rapport au design.

Il n'y en a pas un plus rigoureux que l'autre à mon sens.

Pour les gens du hard, oui, emulateur sous entends "emulateur hardware", et effectivement, tu ne peux pas te tromper sur la facture (cf. les émulateurs celaro à 5 millions d'euros ...)

Dans le domaine du soft, le terme "emulateur" est très courrament employé pour désigner ce que les hardeux appellent simulateurs.

Moralité : Les informaticien et les élèctroniciens ne parlent pas la même langue, c'est tout ;-)

[ Dans le même registre, parler de verification, de validation, puis de test successivement à un informaticien puis à un élèctronicien pour voir la différence ;-) ]

> Comme VMWare/plex86 tourne comme une simple application

Je crois que ce n'est pas tout à fait vrai : Plex86 a besoin d'ajouter un module au noyau, donc, il y a quand même un bout qui tourne en kernel mode. (Ce qui fait que malheureusement, on peut faire crasher tout le système avec un plex86 instable.)

> user, tu lances /usr/local/OpenOfficeRC1/setup

Je dirais même plus : en user, tu lances n'importe quel composant OOo et il lance le setup tout seul.

tar xzvf fichier.tar.gz

puis lis les commentaires du thread précédant (install et setup)

Pour de l'embarqué, les solutions sont en général à base de SoC (System on Chip), qui contiennent plusieurs modules, dont certains spécifiques (algo codé en dur) et certains programmables (processeurs génériques ou spécialisés). Pour la partie programmable, il y a un bout de logiciel qui est stoqué dans une ROM flashable à l'intérieur ou à l'extérieur de la puce, donc, si c'est programmable, c'est aussi reprogrammable.

Pour les parties matérielles spécifiques (moins flexibles, mais super efficace au niveau performances), il n'y a plus grand chose à faire après la sortie de la fab.

Ce qui serait bien, c'est d'avoir une puce avec tous les alogs communs mp3/OGG en matériel et le reste en logiciel, pour pouvoir faire les deux avec le moins de surface de sillicium possible. Mais les algos sont peut être trop différents ...?

L'autre solution est que le Hardware lui-même soit reprogrammable. (Solutions à base de FPGA) Les spécialistes de la question en parlent de plus en plus et beaucoup pensent que c'est l'avenir de l'embarqué, mais pour l'instant, ca n'est pas très développé.

< mode pinaillage >
> Il ne sagit bien sur que des fichiers soumis au copyright bien sur ...

Soumis au copyright et sans une licence autorisant la redistribution

Sinon, la plupart des LL sont copyrightés.

< /pinaillage >