Thomas Douillard a écrit 9175 commentaires

Boarf, les trolls à l'assemblée, c'est monnaie courante, je crois même qu'ils sont plus forts que nous.

Un petit troll distrib' entre un sur le budget de l'éducation nationale et un autre sur la dernière petite phrase du ministre de l'intérieur la police ça serait peut être rafraîchissant ?

... à moi, c'est les conséquences d'un éventuel plantage d'ooffice.

Le grand public se fout du format de publication, ce qu'il veut c'est un truc qui marche sans qu'il ait à se prendre la tête.

Et c'est compréhensible, il veut écouter la radio, pas se plonger dans les arcanes de l'informatique. Si c'est plus compliqué que d'utiliser sa bonne vieille radio, il y a toutes les chances qu'il laisse tomber.

Merci pour les infos, mais c'était plus pour titiller un peu Ernest H qu'autre chose, un "utf-8 possède des limitations" c'était un peu court comme argument à mon sens ;)

D'ailleurs : appliqué à irc ça ressemble pas trop à des limitations.
Ça demande au pire un peu de bande passante en plus à certains serveurs. Rien de bien méchant, donc, je pense pas que les serveurs irc soient facilement saturés.

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)

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.

Les XPs n'existent pas.

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.

C'est aux filles de se faire leur défouloir si elles veulent :)

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 :)

Normalement, ici, il suffit de prononcer le mot [pub] pour se faire jeter à coup de moissages, et lapider à coup de commentaires.

Là non seulement c'est une pub qui s'affiche, mais en plus le site à l'air de marcher du tonnerre ! C'est magique.

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 ...

Euh, si, elle s'applique, mais elle est pas très contraignante. Tant que veux pas redistribuer en tout cas.

C'est sans doute parce que je prends pas le sujet très au sérieux ;) C'est un faux coup de geule.

Sauf que l'ascii ne gérait bien qu'un nombre limité de caractère, adapté à l'anglais on va dire.

Les multiples encodages qui sont arrivés après sont arrivés justement pour cette raison, dont un nombre incalculable de variations de l'ascii.

L'utf-8 est peut être une monoculture, mais il n'est plus tellement spécifique à l'anglais ...

Enfin, l'argument des clients qui gèrent pas utf-8 est bidon : ils sont à ma connaissance plus nombreux que ceux qui gèrent l'encodage par chan avec lequel "tu fais pas chier le monde" ;) Non, c'est le monde qui te fais chier à obliger de configurer ton client :)

Peut être que c'est le protocole qui est à jeter, en fait.

Sinon, c'est quoi les limitations d'utf-8 ?

Parce que ça fait chier de changer la config par défaut à chaqur fois qu'on change de machine/client ? Parce que sur freenode par exemple, tous les chans peuvent avoir des préférés par défaut différents, et que tous les clients gèrent pas un charset différent par chan, mais que tous les clients ou quasiment gèrent l'utf-8 ? Ca serait quand même nettement plus simple pour ceux qui traînent sur des chans internationaux qu'ils soient tous en utf-8.

Et enfin, parce que c'est pas compliqué de passer un chan irc en utf-8, bordel de merde ? Nettement moins usant que de kicker les nouveaux 15 fois par jour. Peut être que c'est moins glorifiant de ne rien avoir à profiter du pouvoir d'être op (que je ne qualifierai pas :p) ?

T'as des protocoles de routage IP, pour ça effectivement (me demande pas les noms, je me fais une joie de pas les connaître/ les avoir oubliés)
D'ailleurs c'était dans le cahier des charges initial de l'armée d'avoir un réseau robuste, si je me trompe pas.

Peut être que Renater les utilise pas pour une raison que j'ignore ...

Du bavardage vide ton commentaire.

Eh non ! à la fin, on est aussi contre ce pourquoi LePen est pour, donc on est pour personne.

Sauf si on est aussi contre le fait d'être pour personne. Dans ce cas, on est forcément pour quelqu'un quand même. Sauf si ...

Moralité : être contre tout, c'est un peu ne pas avoir d'avis.

Bon, si le coup d'état est une solution, faut y aller ! et surtout faire mieux après.

Tu sais, rien n'interdit à un ministre de l'écologie : ministre -> besoin de comprendre la politique, et écologie -> besoin de comprendre ... l'écologie, de s'entourer de gens compétents en science/écologie/...

Sinon, comment tu veux éviter de te faire bouffer par tel autre ministre qui a besoin de soux pour calmer des profs pas contents ou pour boucher le trou de la sécu ?

En même temps, dans un système démocratique, la seule manière de changer un système c'est de jouer le jeu dudit système ...

T'as bu trop de kiklenny ... kileklinny ... bière toi

Parce que ça peut être utile et pratique ?

Les devs, ils deviendrons des dinausores ou ils comparerons à l'usage ce qui est le plus pratique à utiliser pour ce qu'ils ont à faire.
Wait & see donc.

Non, je n'ai pas de problème avec les chaines de caractères en C, c'est juste particulièrement lourd à manipuler dans ce langage (Honnêtement, je crois pas connaître pire, d'après des retours que j'ai eu appliquer une regexp en C c'est d'une lourdeur totale, par exemple, pour concaténer deux chaines il faut appeler une fonction, se demander si la fonction en question alloue elle même la mémoire ou si elle attends la place nécessaire préallouée ... Alors qu'en shell, tu feras pas grand chose sans manipuler des chaines de caractères.

Pour la compilation : cet exemple était certe pourri, j'avais prévenu ;) Mais je déteste pas faire des trucs un peu élaboré avec un shell, ou utiliser des boucles for ou des trucs dans ce genre. Ce qui est frustant dans ce cas, c'est le nombre de tricks qu'il faut se rappeler pour faire marcher le bouzin correctement alors que c'est 5 lignes de code ... je pense perso que l'approche "une entité du SE", un fichier par exemple, est un objet, avec immédiatement et facilement accessible tout ce qu'on voudrait en savoir, comparée à l'approche "une entité est une chaîne" avec des commande à taper et des lignes de textes de descriptions accessibles à partir de commande qui prennent en paramètre l'identifiant chaine de l'entité qu'il faut parser derrière est bien meilleure.


Pour le séparateur par défaut, le changer, c'est du bricolage, et oui, je savais qu'on pouvait le faire. C'est de la trituration mentale de se demander à chaque fois dans quel cas ça va foirer et ce qu'il faut faire pour y remédier, mettre des quotes, utiliser $@ etc.


Je me jette pas à corps perdu dans cet outil, j'ai déja dit que je m'en foutais un peu. D'ailleurs j'utilise pas windows.

Sur les fonctions et attributs, là tu te plantes : on a déja dit que grâce à l'introspection des objets, tu pouvais connaître en ligne toutes les méthodes que tu peux leur appliquer, type shell completion, éventuellement avec la doc j'imagine. Le genre de trucs qui peuvent faciliter la vie.


Mais après, si "ça sert à rien, on pouvait déja faire ça avec Y" et "on pouvait faire ça en C aussi", j'ai plus rien à ajouter à mon premier post, rendez-vous dans quelques temps ;)