informatique/autodidacte-apprendre la manipulation de bits

Le 23-06-2010, Antoine Leca <root@localhost.invalid> a écrit :

Marc Boyer écrivit :

En physique non plus on a pas trop de moyen de prouver que les choses
marchent,

Euh... il a quand même fallu attendre attendre un certain IN pour avoir
une preuve permettant de savoir pourquoi les choses _tombaient_, ce qui
pourtant sensiblement plus simple que marcher. Avant IN, les choses
tombaient... de par leur « vertu tombante » (Aristote)

et pourtant, il me paraît plus facile d'y faire des choses robustes.

Bin voilà, comme disait l'autre, « du haut de ces pyramides, ... »
Y'a pas à dire, 42 (ou 43) siècles, cela aide !

Oui, l'informatique est une science jeune. C'est exitant mais
moins balisé.
Et on se pose encore des questions du genre: "est-ce fragile
par nature ou par mauvaise ingénierie ?".

"au temps des cartes perforées, on réflechissait avant d'éxecuter
son code").

Pas sûr. Mais on réfléchissait surtout avant de pondre son code, parce
que le délai entre le moment où l'analyste écrivait le code sur sa
feuille, et le moment où on lui rendait le listage de compilation,
pouvait être de plusieurs... jours : eh oui, il fallait passer par le
programmeur, qui traduisait en lignes de code, puis par le, ou plus
souvent /la/, perforatrice pour faire la pile de cartes, puis trouver un
moment sur la bécane pour faire tourner le job de compilation, puis un
autre moment sur la bécane annexe pour faire tourner le job
d'impression, et ensuite passer la tête au service chargé de la
distribution des listages.

J'ai fais là une petite digression, mais je ne cautionne pas du
tout les propos raportés. On délègue de plus en plus de travail
à la machine, et la productivité augmente. S'il fallait encore 2 jours
pour compiler 200L de code, on aurait pas d'informatique grand
public.
C'est aussi pertinent que de regretter les enluminures tuées
par l'imprimerie.

Mais remarquez bien qu'aujourd'hui, les nouveaux matériaux n'empêchent
pas les architectes de bien mieux savoir qu'avant pourquoi les immeubles
tiennent debout : les progrès ont lieu tant dans les techniques que dans
la partie théorique du génie civil. Cependant, cela n'a pas fait revenir
en arrière sur les règles de sûreté qu'ont imposées l'expérience, et en
particulier sur les coefficients (2 ou le plus souvent 3) que l'on
applique en génie civil : un peu comme la méthode qui consiste à
programmer le même sous-système plusieurs fois et à arbitrer ensuite les
résultats (c'est bien comme cela que fonctionne un avion, non ?)

Oui, globalement, un avion fonctionne comme ça. En ce qui
concerne les commandes de vol d'un Airbus, on a même 10 CPU
qui font la même chose, et entre 2 et 5 codes distincts
(toutes les infos ne sont pas publiques).

Marc Boyer
--
En prenant aux 10% des francais les plus riches 12% de leurs revenus,
on pourrait doubler les revenus des 10% les plus pauvres.
http://www.inegalites.fr/spip.php?article1&id_mot0

Marc Espie a écrit :

C'est tres proche des resultats d'indecidabilite en informatique. Plus
precisement, tu noteras que des qu'on commence a raisonner sur une theorie/une
preuve (e.g., un algorithme, la semantique d'un programme), alors on ne
sait rien faire des qu'on travaille avec une theorie utile (contenant
l'arithmetique) -> en informatique, tout probleme "non trivial" en particulier
raisonnant sur de la correction de programme, est indecidable.

Juste un petit bémol souvent oublié: en pratique en informatique on
travaille sur une arithmétique finie (allez 32bits) et tous les
problèmes d'indécidabilités (théoriques) de l'arithmétique de Goedel
s'évanouissent.

Bon par contre pour prouver que le prog fini s'arrête ou boucle, on peut
parcourir un nombre faramineux de positions de l'espace des états, ce
qui est difficile. Mais une chose est sure: les théorèmes mathématiques
sur les ensembles infinis ne s'appliquent pas forcément à l'identique
sur les ensembles finis.

Les maths parlent parfois de chose qui n'existent /pas vraiment/ (cf
l'hôtel de Hilbert, dont on attends toujours l'adresse[*]), mais ca ne
les rends pas moins inintéressantes, mais il faut séparer la théorie (on
accepte "l'infini") et la pratique (tout est fini en se bas minde).
____
[*] pour s'inspirer d'Harry Potter et des numéros de quais
fractionnaires, il parait que cet hôtel se situe précisément en face du
numéro Omega-de-Chaitin rue Archimède.

Tu peux en general t'en sortir en "bornant tout".

Tout a fait, et en pratique ce qui contient une mémoire dans l'ordi est
toujours fini. Ca peut être gros bien entendu, mais il y a des CPUs avec
seulement quelques octets de ROM et de RAM aussi (celui qui fonctionne
dans la machine à laver ou le micro-onde).

Mais c'est pas simple: meme

si ton programme est fini, il peut contenir des boucles infinies (non bornees
en temps), et ca suffit a foutre la merde.

Normalement dans l'espace des états il faut aussi inclure les registres
du CPU, et une boucle infinie se traduit par le fait qu'on se retrouve
dans un état précédemment vu: le compteur programme est identique, les
autres registres aussi ainsi la mémoire vive et celle de masse.

Je ne sais pas si cela a été fait, mais un CPU 4 bit, avec 32 bits de
ram (quel luxe) et autant de ROM qu'on veut (car elle ne fait pas parti
de l'espace des états) doit être explorable dans son entier avec des
techniques adaptées, BDDs et autres SAT-solvers j'imagine.

Je m'insurgeais dans un message precedent sur le fait qu'on n'a pratiquement
pas d'outil industriel s'appuyant sur ce genre de choses. Idealement, il
faudrait pouvoir isoler dans un programme les bouts de code "dangereux"
(non bornes) sur lesquels on ne va pas pouvoir raisonner.

Il y a quand même des trucs qui industriellement on eu un succès. La
méthode B par exemple.. même s'il faut des bac+5/6/7/8 en post-doc pour
pouvoir travailler avec car c'est vraiment pas pensé pour être pratique
et simple pour les gens standard (ce qui est une grosse erreur à mon
avis pour une acceptation par les opérationnels).

Dans ce que j'ai vu, tu as d'une part la theorie: formalisme comme esterel
a portee tres limitee, ou langage qui n'est pas sorti du labo, et la
pratique: langage a la C/java, avec des "outils" de verification qui au final
te sortent des resultats pathetiques de faiblesse (style: il y a *peut-etre*
un buffer overflow a la ligne xxxx).

Tu peux utiliser des langages de plus haut niveau pour éviter cela.
L'erreur est peut-être de vouloir faire de la preuve sur des langages
bas-niveau alors qu'on peut faire des trucs puissant sur des langages
plus abstraits. La programmation devenant alors plutôt un truc
conceptuel proche des mathématiques façon "B".

sam.

In article <4c2333c5$0$17284$426a74cc@news.free.fr>,
Samuel DEVULDER <samuel-dot-devulder@laposte-dot-com> wrote:

Marc Espie a écrit :

C'est tres proche des resultats d'indecidabilite en informatique. Plus
precisement, tu noteras que des qu'on commence a raisonner sur une theorie/une
preuve (e.g., un algorithme, la semantique d'un programme), alors on ne
sait rien faire des qu'on travaille avec une theorie utile (contenant
l'arithmetique) -> en informatique, tout probleme "non trivial" en particulier
raisonnant sur de la correction de programme, est indecidable.

Juste un petit bémol souvent oublié: en pratique en informatique on
travaille sur une arithmétique finie (allez 32bits) et tous les
problèmes d'indécidabilités (théoriques) de l'arithmétique de Goedel
s'évanouissent.

Merci d'enfoncer des portes ouvertes...

Bon par contre pour prouver que le prog fini s'arrête ou boucle, on peut
parcourir un nombre faramineux de positions de l'espace des états, ce
qui est difficile. Mais une chose est sure: les théorèmes mathématiques
sur les ensembles infinis ne s'appliquent pas forcément à l'identique
sur les ensembles finis.

Deuxieme porte ouverte.

Bon, on va continuer sur les portes fermees, pour changer.
Sur le chemin de l'indecidabilite, la lecon la plus importante, c'est la
facon dont tu obtiens ces resultats. Ca te dit de facon tres claire qu'il
n'y a pas de facon de "simplifier" les choses. Applique a de l'informatique
finie, ca te dit juste qu'il va falloir se manger tout l'espace d'etats,
qu'il n'y a pas de facon d'en faire (beaucoup) moins... donc qu'en pratique,
c'est mort...

Les maths parlent parfois de chose qui n'existent /pas vraiment/ (cf
l'hôtel de Hilbert, dont on attends toujours l'adresse[*]), mais ca ne
les rends pas moins inintéressantes, mais il faut séparer la théorie (on
accepte "l'infini") et la pratique (tout est fini en se bas minde).

Pas du tout d'accord avec toi. Si tu es intuitionniste, tu peux eventuellement
considerer que les objets non constructibles n'existent pas, mais l'infini
mathematique est quelque chose de parfaitement concret et utilisable.

Tu connais le mythe de la caverne ? le monde que tu vois n'est qu'une
projection limitee de la realite (en particulier, l'esprit humain a un
peu de mal a apprehender l'infini).

Dans ce que j'ai vu, tu as d'une part la theorie: formalisme comme esterel
a portee tres limitee, ou langage qui n'est pas sorti du labo, et la
pratique: langage a la C/java, avec des "outils" de verification qui au final
te sortent des resultats pathetiques de faiblesse (style: il y a *peut-etre*
un buffer overflow a la ligne xxxx).

Tu peux utiliser des langages de plus haut niveau pour éviter cela.
L'erreur est peut-être de vouloir faire de la preuve sur des langages
bas-niveau alors qu'on peut faire des trucs puissant sur des langages
plus abstraits. La programmation devenant alors plutôt un truc
conceptuel proche des mathématiques façon "B".

Le probleme, c'est surtout que tu pourrais avoir un langage de bas niveau,
avec des annotations relativement simples indiquant que telle zone est
"neuneu" et donc prouvable (et l'enseignement qui va avec pour avoir du
developpeur qui ne fait pas n'importe quoi).

Avec un peu de bol, si les multi-coeurs se generalisent, on va voir le
retour du fonctionnel (comment eviter les locks: facile, suffit de ne
pas avoir de valeur mutable). Mais ca c'est mon cote optimiste.

Mon cote pessimiste me dit qu'on va avoir de plus en plus d'applications
bugguees tellement tu peux faire confiance a l'informaticien moyen pour
faire du multi-threads alors qu'il n'a aucune chance de le faire marcher
correctement.

Marc Espie a écrit :

Sur le chemin de l'indecidabilite, la lecon la plus importante, c'est la
facon dont tu obtiens ces resultats. Ca te dit de facon tres claire qu'il
n'y a pas de facon de "simplifier" les choses. Applique a de l'informatique
finie, ca te dit juste qu'il va falloir se manger tout l'espace d'etats,
qu'il n'y a pas de facon d'en faire (beaucoup) moins...

Ah? jamais entendu parler des abstractions des espaces d'états? Si tu
montre sur un sur-ensemble de l'espace d'état que ca ne boucle pas,
alors sur l'espace d'état réel ca ne bouclera pas plus. C'est aussi vrai
pour le bouclage que pour n'importe quelle autre propriété. Sujet
voisin: l'utilisation des implicants dans les Sat-solvers et les
méthodes de model checking à base de BDD. Sur certains espaces d'états
ces techniques marchent super bien. Pourquoi s'en priver et jeter le
bébé avec l'eau du bain?

L'indécidabilité de l'arrêt parle de toutes les machines de Turing, mais
ne dit rien quant aux machines de moins de 256 états (n'importe quel
nombre convient). Cela signifie qu'on peut parfaitement trouver des
technique pour vérifier un programme réel non arbitrairement gros et
éventuellement soumis à des contraintes.

donc qu'en pratique,

c'est mort...

En pratique, dans de nombreux projets européens et instituts de
recherches, il y a a pas mal d'approches pour écrire des programmes plus
robustes, ou pour tester la robustesse des programmes. Ca n'est pas
parce que la théorie nous dit qu'on ne peut pas pour *tous* les
programmes qu'on ne le peut pas pour une classe particulière.

Allez: un peu de concret pour changer du défaitisme des théoriciens qui
maintiennent les portes fermées. Regarde du coté de l'outil Agatha au
CEA. Et ça n'est qu'un exemple parmi d'autres que j'ai croisé, il y a
sans doute mieux ailleurs (j'avais cité cbmc si mes souvenirs sont bons).

Pas du tout d'accord avec toi. Si tu es intuitionniste, tu peux eventuellement
considerer que les objets non constructibles n'existent pas, mais l'infini
mathematique est quelque chose de parfaitement concret et utilisable.

Pas pour l'usage commun! Très peu de développeurs en informatique n'ont
besoin de manipuler l'infini concrètement. Je ne dis pas que l'infini
n'existe pas ou que l'utilisation de l'axiome du choix conduit à
raisonner sur des choses qui n'existent pas (quoique... j'ai de serieux
doutes sur l'existence réelle des boules du paradoxe de banach-tarski).
Je dis juste qu'en pratique, ce qu'on nous raconte sur les objets et
construction intellectuelles infinies, c'est pas forcément (toujours)
applicable aux objets finis.

Tu connais le mythe de la caverne ? le monde que tu vois n'est qu'une
projection limitee de la realite (en particulier, l'esprit humain a un
peu de mal a apprehender l'infini).

Oui sans doute. Mais je pense que quoi qu'on fasse, quoi qu'on dise on
ne traite jammais que des objets finis dans le monde reel. Aussi
j'aimerais bien qu'on me montre l'utilité *pratique* de l'infini
dénombrable en informatique. Ca m'intéresse beaucoup.

Dans ce que j'ai vu, tu as d'une part la theorie: formalisme comme esterel
a portee tres limitee, ou langage qui n'est pas sorti du labo, et la
pratique: langage a la C/java, avec des "outils" de verification qui au final
te sortent des resultats pathetiques de faiblesse (style: il y a *peut-etre*
un buffer overflow a la ligne xxxx).

Tu peux utiliser des langages de plus haut niveau pour éviter cela.
L'erreur est peut-être de vouloir faire de la preuve sur des langages
bas-niveau alors qu'on peut faire des trucs puissant sur des langages
plus abstraits. La programmation devenant alors plutôt un truc
conceptuel proche des mathématiques façon "B".

Le probleme, c'est surtout que tu pourrais avoir un langage de bas niveau,
avec des annotations relativement simples indiquant que telle zone est
"neuneu" et donc prouvable (et l'enseignement qui va avec pour avoir du
developpeur qui ne fait pas n'importe quoi).

Je connais des langages de bas niveau comme ca: les machines à états
finis. Après ca dépendra de leur langage d'action. Mais certains
langages d'action permettent de faire des choses rigolotes comme encoder
des protocoles de communication, de la gestion de paquets TCP/IP, etc.
Pas mal de truc utiles quand même.

Avec un peu de bol, si les multi-coeurs se generalisent, on va voir le
retour du fonctionnel (comment eviter les locks: facile, suffit de ne
pas avoir de valeur mutable). Mais ca c'est mon cote optimiste.

Pas de valeur mutable? J'imagine que l'espoir viendra des choses
scheme-like alors. Vive le "let"! A noter que je constate perso que dans
les langages à objets qui manipulent de l'information et pas des
nombres, beaucoup de variables sont en réalité des constantes dans les
programmes. A tel point qu'en java par exemple ca aurait été bien
d'avoir à déclarer var pour indiquer une vraie variable et qu'il y ait
un final implicite pour tout le reste. Avec en plus le fait que le
compilo pourrait intuiter le type du final automatiquement. Mais bon
c'est un autre sujet.

Mon cote pessimiste me dit qu'on va avoir de plus en plus d'applications
bugguees tellement tu peux faire confiance a l'informaticien moyen pour
faire du multi-threads alors qu'il n'a aucune chance de le faire marcher
correctement.

Tu sembles très pessimiste en effet tu sais. Les gens sont plus
intelligents que tu ne le penses, enfin j'espère!

sam (qui n'a plus le moral, Marc lui a foutu le bourdon, snif).

Le 23-06-2010, Marc Espie <espie@lain.home> a écrit :

In article <hvt7ci$nbt$1@news.cict.fr>,
Marc Boyer <Marc.Boyer@cert.onera.fr.invalid> wrote:

Le 18-06-2010, Antoine Leca <root@localhost.invalid> a écrit :

Idem pour les algorithmes réseau : on utilise un modèle de faillites
possibles, qui définit des tolérances, et quand on sort on décide qu'il
s'agit d'une vraie défaillance.

Oui, mais ils sont bien plus compliqués que les algorithmes centralisés.

Il y a une robustesse à base de save/restore/retry relativement facile
à mettre en oeuvre, qui améliorerait l'état actuel déjà. C'est d'ailleurs
cette mise en oeuvre au niveau admin système qui, à mon sens, permet
de tolérer les bugs dans les systèmes sans interraction avec le monde
physique (on sait sauvegarder l'état d'un système informatique). Il s'agit
d'intégrer cela dans la programmation des systèmes/applications.

Ca a l'effet pervers d'encourager les bugs "legers" jusqu'a ce que ca
devienne des bugs graves.

N'est-ce pas le cas de tous les systèmes d'aide ? Du ramasse miette
(qui dispense de réfléchir à son utilisation mémoire) à l'ABS ("mais non,
je le colle pas trop, j'ai l'ABS").

En fait, tout bon mecanisme de monitoring se doit d'avoir un postmortem
le plus precis possible (et celui-ci doit etre utilise pour corriger les
bugs!). Redemarrer le systeme "sans comprendre", ce qui est helas monnaie
courante, c'est un peu comme apprendre la conduite a un singe...

Oui, de même qu'en physique, on sait que les systèmes "travaillent",
mais on les passe à la loupe de temps en temps.

Marc Boyer
--
En prenant aux 10% des francais les plus riches 12% de leurs revenus,
on pourrait doubler les revenus des 10% les plus pauvres.
http://www.inegalites.fr/spip.php?article1&id_mot0

Le 24-06-2010, Marc Espie <espie@lain.home> a écrit :

Dans ce que j'ai vu, tu as d'une part la theorie: formalisme comme esterel
a portee tres limitee, ou langage qui n'est pas sorti du labo, et la
pratique: langage a la C/java, avec des "outils" de verification qui au final
te sortent des resultats pathetiques de faiblesse (style: il y a *peut-etre*
un buffer overflow a la ligne xxxx).

Tu peux utiliser des langages de plus haut niveau pour éviter cela.
L'erreur est peut-être de vouloir faire de la preuve sur des langages
bas-niveau alors qu'on peut faire des trucs puissant sur des langages
plus abstraits. La programmation devenant alors plutôt un truc
conceptuel proche des mathématiques façon "B".

Le probleme, c'est surtout que tu pourrais avoir un langage de bas niveau,
avec des annotations relativement simples indiquant que telle zone est
"neuneu" et donc prouvable (et l'enseignement qui va avec pour avoir du
developpeur qui ne fait pas n'importe quoi).

A ma connaissance, des outils de preuve automatique sont utilisés
dans l'industrie aéronautique (http://www.astree.ens.fr/). L'idée
est plutôt de prendre le langage C, mais de restreindre l'usage
que de définir un nouveau langage.
Sinon, comme déjà dit, il y a les langages synchrones, mais ils
ne sont pas adapté à tout.

Avec un peu de bol, si les multi-coeurs se generalisent, on va voir le
retour du fonctionnel (comment eviter les locks: facile, suffit de ne
pas avoir de valeur mutable). Mais ca c'est mon cote optimiste.

Personne ne sait vraiment ce qu'il va advenir des multi-coeurs.
AMHA, à 4 coeurs, on reste sur de la programmation classique, avec un
coeur par appli (firefox sur un coeur, eclipse/word/VC++ sur un autre,
et les deux autres qui font ce qui reste).

Après, on a des retours des SIMD avec les GPU, et en gros 2-4
coeurs généralistes, et plein de petits coeurs dédiés à la 3D
ou au calcul scientifique.

Est-ce qu'on aura des 8-16 coeurs généralistes ? Ca impliquerait
en effet un changement de paradigme de programmation.

Mon cote pessimiste me dit qu'on va avoir de plus en plus d'applications
bugguees tellement tu peux faire confiance a l'informaticien moyen pour
faire du multi-threads alors qu'il n'a aucune chance de le faire marcher
correctement.

Et on peut retrouver un Save/Kill/Restore tellement les bugs liés
à la concurrence sont "aléatoires" (avec une définition adéquate de l'aléa).

Marc Boyer
--
En prenant aux 10% des francais les plus riches 12% de leurs revenus,
on pourrait doubler les revenus des 10% les plus pauvres.
http://www.inegalites.fr/spip.php?article1&id_mot0