thoasm a écrit 9443 commentaires

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

Tu peut construire à la mimine ta valeur, et faire un "get-process ma_valeur_construite_a_la_mimine" j'imagine ... et si le process existe pas, get-process doit te l'indiquer. (j'ai cru entendre parler d'exceptions)

je le fais en c

Tu passes du bash au C directement ? La vache. C'est complètement orthogonal du point de vue gestion des chaines de caractères, et d'un tas d'autres choses d'ailleurs. Ça explique bien des choses ;)

Et pour ton fichier de compilation séquentiel
Pourquoi pas un truc du genre

a_compiler = { fichiers compilables du répertoire }

Pour chaque fichier de a_compiler
Si fichier.est_lisible() alors
fichiers_objets.ajouter = fichier.compiler()
fin si
fin pour

executable = fichiers_objets.lier()

avec la gestion des erreurs, et tout ? j'adorerai faire ça ... sans avoir à gérer mon ensemble de fichier comme une chaine de caractère bash dans laquelle un espace dans le nom de fichier foutra la merde ou connaitre la manpage de "test" par coeur pour savoir si un fichier est plus récent qu'un autre ...

Ok, c'est complètement farfelu comme exemple, c'est surement pas réalisable cash, vaut mieux faire un makefile, mais c'est pour donner une idée.

Et de renchérir : surtout quand la qualité bash/ksh/... vs cmd.exe, completion, efficacité du shell a longtemps été un sujet de raillerie de la part des linuxiens vis à vis de windows. Là sur le shell lui même ils ont pas grand chose à envier, au contraire.

Ton commentaire ressemble surtout à celui d'un mec vexé qui veut pas perdre la face. "oué, ok il ont sorti un truc bien. Mais quand même". Et ça, c'est parce que c'est MS, j'en suis profondément persuadé.

... Sauf que c'est pas des fonctionnalités qu'on parle, c'est du principe du shell. Imagine les fonctionnalités des commandes combinées avec le shell lui même ?

Ça ça existe déja, c'est ipython je crois. Mais iphython ce n'est pas encore tout à fait ça: il manque notament l'accès "de base" a pleins d'objets système, applis, ... pour pouvoir scripter tout ça et accéder à pleins de trucs, de piper des objets (cf les exemples), ...

Ca n'a rien a voir avec les fonctionnalités ou le nombre de commande, c'est simplement un moyen d'accéder à ces fonctionnalités.