informatique/autodidacte-apprendre la manipulation de bits

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

Problèmes d'encoding?

Pas d'accents. Surtout UTF8.

Mais c'est du grand n'importe quoi, ce que tu affirmes !

Si c'est toi qui le dis.

Pareil, la-aussi.

Quoi? Que le problème de l'arrêt n'est pas un problème pratique. Oui
parfaitement. Je rejoins Marc là dessus: Les problèmes non décidables ne
sont pas des problèmes pratiques dans la vie industrielle où les choses
sont finalement bien plus simples que ca.

Okay, meme apres un message entier a t'expliquer pourquoi tu en as tout
le temps des problemes indecidables, tu ne les vois toujours pas ?

Le probleme de l'arret, c'est l'exemple simple qu'on donne aux gens.
Le theoreme suivant dit en gros que les problemes informatiques se separent
en deux categories, les problemes triviaux, et les problemes indecidables
(en nuancant un peu, tu as les problemes triviaux, les NP-complets, et
les indecidables). Une des particularites, c'est que quasiment tout ce qui
est "meta" est indecidable. Dire si un programme s'arrete -> indecidable,
*DIRE SI UN PROGRAMME EST SANS BUG* -> indecidable. Dire si un programme ne

Juste une question bête: c'est quoi ta définition d'un prog sans bug? La
mienne est celle d'un prog fidèle aux specs. Le soucis c'est que les
specs c'est du langage +/- naturel bourré d'implicite, de non-dits, et
de choses ambigües. On attends toujours et encore une façon d'écrire
des specs qui tiennent la route par rapport à cela.

Et on attend encore une facon d'ecrire les programmes qui tienne la route,
independamment des specs.

va pas planter pour cause de division par zero -> indecidable.

Indécidable dans le cas *général*, mais en pratique on ne travaille que
sur des cas particuliers. La théorie de l'indécidabilité dit qu'on ne
peut pas dire si un prog quelconque parmi tous les programmes de taille
arbitraires, bref un prog tiré au hasard ne va, par exemple, boucler.

Indecidable dans tous les cas pratiques que tu vas rencontrer, parce que
justement tes langages ne limitent pas ce que tu fais, et donc que tu
ne peux *pas* analyser ton code.

La pratique de l'indecidabilite te dit que tu ne sais pas si un programme
qui fait un truc interessant ne va pas boucler.

La pratique de la programmation en vrai te dit que tout programme reel
sur lequel on n'a pas pu faire tourner de moulinette capable de le
verifier automatiquement contient des boucles infinies (c'est-a-dire,
l'immense majorite des programmes un tant soit peu complexes, qui depassent
les 500 lignesd de code, a vue de pif).

Très bien.. mais en pratique les progs ne sont pas écrit au hasard. Ils
répondent à un cahier des charges, font des choses, et même que parfois
on impose des règles d'écriture. Par exemple interdiction d'utiliser des
while, des goto, de la récursivité, des allocations dynamiques. Seules
les boucles for() bornées en nombre de tour (les boucles "for" du
langage pascal typiquement) ne sont utilisables. Ces règles pratiques
font que dans les domaines où elles sont appliquées le pb de l'arrêt est
un truc de théoricien et pas de praticien.

Tout ceci ne sert a rien, parce que ces criteres sont verifies par des
humains, donc faillibles. Ca va diminuer la proportion de bugs, mais pas
les eliminer.

Le rapport avec la programmation reelle ? Il n'y a pratiquement *aucun*
langage industriel qui se preoccupe de ses meta-considerations. Typiquement,

Bien entendu, ca n'est pas leur boulot. Ils ne sont pas là pour cela.
Ils sont là pour traiter des problèmes concrets, pas des trucs méta.

Ce que je traduis en: ils sont la pour permettre de pisser du code qui
fait semblant de marcher, au moindre cout, sans aucun garde-fou, et avec
d'enormes garanties que tu vas avoir des bugs dedans, et que le systeme
laisse tout passer.

ils sont tous Turing-complets, tout le temps, que tu sois en train de
resoudre des problemes triviaux, ou des problemes impossibles.

Mais on dit la même chose alors? Du coup je ne comprends pas ton "C'est
du grand n'importe quoi" initial ? Une (mauvaise) habitude de langage?

En particulier, tu n'as pas de facon de dire *OKAY, LA J'AI UN ALGO

ELEMENTAIRE,

J'AIMERAIS BIEN RESTER DE FACON CERTAINE DANS LA PARTIE DE L'INFORMATIQUE
SUR LAQUELLE ON SAIT RAISONNER*.

Bien sur que si. Les standards de codage existent et servent en partie à
cela. L'informatique industrielle ne traite pas de l'informatique *en
général* mais de trucs plus simples et maitrisés. Tu ne vas pas mettre
dans un ECU de portière de voiture du code qui va chercher à résoudre
une conjecture mathématique dont on ne sait pas dire si elle est
décidable ou pas.

Les standards de codage te servent a faire une approximation de ca.
Est-ce que tu sais verifier que tes standards de codage sont suivis
(de maniere automatique, hein, sinon c'est faillible) ?
Est-ce que tu peux prouver que tes standards de codage t'apportent
un peu de fiabilite ?

Moi j'en reviens toujours au meme souci. Si tu programmes n'importe comment,
ca passe. Si tu veux programmer mieux, ca coute abominablement cher, parce
que tout est fait a la main. Pourtant, on sait plein de choses sur ce qu'on
pourrait automatiser, mais ca ne se fait pas...

je vois plein de raisons economiques a ca... mais c'est pas parce qu'on fait
toutes les verifications qui coutent cher, c'est bien plus parce qu'on
laisse sortir de la merde bugguee en permanence.

Evidemment, je suis biaise: je passe beaucoup plus de temps a lire,
a auditer et a corriger du code qu'a en ecrire. Mais pour moi, l'idee
de pouvoir raisonner sur un programme, voire de pouvoir PROUVER des choses
sur celui-ci, c'est quelque chose qui a des TONNES d'applications tres
pratiques et immediates.

Oui effectivement c'est un biais. En plus je pense que tu dois être
multi-domaine. En pratique, dans un métier la variabilité du code est
plus réduite que ce que tu vois je pense.

Vraisemblablement...

Marc Espie a écrit :

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

Quoi? Que le problème de l'arrêt n'est pas un problème pratique. Oui
parfaitement. Je rejoins Marc là dessus: Les problèmes non décidables ne
sont pas des problèmes pratiques dans la vie industrielle où les choses
sont finalement bien plus simples que ca.

Okay, meme apres un message entier a t'expliquer pourquoi tu en as tout
le temps des problemes indecidables, tu ne les vois toujours pas ?

Ben non parce que le "tout le temps" dont du parles n'est pas ce que je
constate au jour le jour. Il ne faut pas généraliser trop vite.

Juste une question bête: c'est quoi ta définition d'un prog sans bug? La
mienne est celle d'un prog fidèle aux specs. Le soucis c'est que les
specs c'est du langage +/- naturel bourré d'implicite, de non-dits, et
de choses ambigües. On attends toujours et encore une façon d'écrire
des specs qui tiennent la route par rapport à cela.

Et on attend encore une facon d'ecrire les programmes qui tienne la route,
independamment des specs.

Heu? Dans les specs tu as par exemple des jeux de tests pour vérifier si
ton prog fait ce qu'il doit faire. Ton jeu de test peut avoir été écrit
indépendamment du langage de prog choisi. Il peut même se faire dans un
formalisme totalement différent de celui choisi pour le codage.
D'ailleurs il se peut que les jeux de tests soient écrits avant même
qu'un langage ait été choisi. Les tests d'une pile de communication sont
faits sans savoir si la pile sera faite en VHDL, en C, ADA ou en ASM..
Ils visent juste à savoir si la pile fait ce que la spec (ie. la norme)
dit qu'elle doit faire.

va pas planter pour cause de division par zero -> indecidable.

Indécidable dans le cas *général*, mais en pratique on ne travaille que
sur des cas particuliers. La théorie de l'indécidabilité dit qu'on ne
peut pas dire si un prog quelconque parmi tous les programmes de taille
arbitraires, bref un prog tiré au hasard ne va, par exemple, boucler.

Indecidable dans tous les cas pratiques que tu vas rencontrer, parce que
justement tes langages ne limitent pas ce que tu fais, et donc que tu
ne peux *pas* analyser ton code.

Les langages non, mais le métier dans lequel tu travaille oui, lui il
peut limiter ton usage du langage.

La pratique de l'indecidabilite te dit que tu ne sais pas si un programme
qui fait un truc interessant ne va pas boucler.

Qu'est-ce que tu appelles intéressant au juste? Pour certains, un simple
filtre numérique qui répond rapidement, un algo d'amélioration d'image
sur une dalle LDC, une pile de communication qui occupe peu de CPU, de
RAM ou de ROM sont des trucs intéressants. Ces choses là ne requièrent
pas de se soucier de l'indécidabilité.

La pratique de la programmation en vrai te dit que tout programme reel
sur lequel on n'a pas pu faire tourner de moulinette capable de le
verifier automatiquement contient des boucles infinies (c'est-a-dire,
l'immense majorite des programmes un tant soit peu complexes, qui depassent
les 500 lignesd de code, a vue de pif).

Non.. j'ai des codes qui contiennent beaucoup plus de lignes que cela et
qui pourtant ne sont pas prêts de partir en boucle.. Ce que tu dis
dépend du domaine et de ce que font tes progs.

Très bien.. mais en pratique les progs ne sont pas écrit au hasard. Ils
répondent à un cahier des charges, font des choses, et même que parfois
on impose des règles d'écriture. Par exemple interdiction d'utiliser des
while, des goto, de la récursivité, des allocations dynamiques. Seules
les boucles for() bornées en nombre de tour (les boucles "for" du
langage pascal typiquement) ne sont utilisables. Ces règles pratiques
font que dans les domaines où elles sont appliquées le pb de l'arrêt est
un truc de théoricien et pas de praticien.

Tout ceci ne sert a rien, parce que ces criteres sont verifies par des
humains, donc faillibles.

Non. Il existe une foultitude d'outil d'analyse de code et qui beepent
dès qu'on s'écarte de la norme de codage. Pas d'intervention humaine
dans ce qu'ils font.

Ca va diminuer la proportion de bugs, mais pas

les eliminer.

Eliminer *tous* les bugs n'a pas de sens. Tu bouges les specs, tu crée
des bugs.

Les standards de codage te servent a faire une approximation de ca.
Est-ce que tu sais verifier que tes standards de codage sont suivis
(de maniere automatique, hein, sinon c'est faillible) ?

Oui.

Est-ce que tu peux prouver que tes standards de codage t'apportent
un peu de fiabilite ?

Oui.

J'ai du mal à comprendre que tu puisse affirmer qu'il soit impossible
d'automatiser la vérification des normes de codages particulière: par
exemple que tu n'as pas plus d'un certain nombre de blocs imbriqués, que
tes boucles for() sont du type "i=0; i<0; ++i" avec une variable "i" qui
n'est pas modifiée par le contenu de la boucle, que ton prog n'ai pas de
goto, de malloc, d'appel recursif, etc. Si tu sors des rails: beep. A
toi de revoir ton codage pour rentrer dans le rang.

Alors bien sur programmer avec ces contraintes c'est moins fun. On est
moins libre de faire ce qu'on veut, mais bon dans l'industrie on est pas
payé pour faire ce qu'on veut justement, mais faire ce qui est prévu
avec les outils disponible dans le métier (un sous ensemble du C par
exemple).

Moi j'en reviens toujours au meme souci. Si tu programmes n'importe comment,
ca passe. Si tu veux programmer mieux, ca coute abominablement cher, parce
que tout est fait a la main. Pourtant, on sait plein de choses sur ce qu'on
pourrait automatiser, mais ca ne se fait pas...

je vois plein de raisons economiques a ca... mais c'est pas parce qu'on fait
toutes les verifications qui coutent cher, c'est bien plus parce qu'on
laisse sortir de la merde bugguee en permanence.

Tout dépend de ce qu'on entends par buggé. Si je te vends une pile de
communication série qui marche jusqu'à 100kbits par secondes. Est-ce que
tu va parler de bug si lorsque tu la fais tourner à 1Mbits/seconde elle
ne marche plus? Bien sur que non. Souvent les bugs constatés sont plus
liées au fait qu'on emploi le soft en dehors de ses specs qu'à un défaut
de codage. Dans ce cas là, il n'y a pas plus de difficultés avec le soft
qu'avec n'importe quel composant physique ou électronique.

sam.

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

Marc Boyer écrivit :

Mais je ne connais pas de problème industriel grave qui soit lié à
un problème de virgule flottante.

Trop gros, ou pas assez grave, le vol L501 ?

Le vol d'ariane qui a explosé ? Oui, ma phrase n'était peut-être
pas assez explicite, mais je ne rangeais pas ça dans les pb
de calcul numérique, convergence and co.

Mais pour en revenir au sujet, qui est de se demander si la fragilité
des codes vient de la nature de l'informatique où juste des méthodes
industrielles, c'est plus à la physique qu'aux maths qu'il faut opposer
l'informatique.

Fragile est le contraire de robuste. Et robuste est un qualificatif que
tu peux appliquer à des démonstrations, à des conjectures...

ok

Et la physique est continue à son échelle humaine industrielle.

Mais pas à l'échelle atomique, ni même microscopique pour certains
phénomènes comme les frottements ; donc ce n'est pas continu au sens
mathématique du terme.

De la même manière, si l'informatique des programmes est effectivement
discrète, lorsque tu t'intéresses à un système informatique dans son
ensemble, tu peux considérer certaines propriétés comme
pseudo-continues:

Ben, c'est là que je ne suis pas sûr que l'analogie passe.
La physique est continue au niveau humain parce que, globalement,
l'état global ne dépend pas de l'état discret d'un unique composant.
Si tu bouges un atome dans une structure, ça n'a pas d'impact
notable sur la structure globale.
Si tu bouges un bit dans une mémoire, ça passe où ça
casse. Un changement discret microscopique a un impact discret
macroscopique.

Elle permet donc des approximations, des marges de tolérance.

Bah ? Si tu permets à un sous-système de diverger jusqu'à un certain
point, et qu'à ce moment-là tu tues le processus et le relances
(technique classique, utilisée par exemple dans le noyau Windows), c'est
exactement la même chose qu'établir des marges de tolérance, non ?

Ça se défend comme point de vue. Mais ce n'est pas vraiment le
paradigme de base. Mais ceci dit, la POO est assez loin de la
machine de Turing, et elle est devenue un paradigme majeur.

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.

Mais si le bug est déterministe, ça ne va pas aider (on revoit
pointer arianne, déjà évoquée en début de message).

Et est-ce qu'on peut aller au delà ? Ca reste très discret à
mon sens.

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

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.

Je veux dire: dans la plupart des circonstances, monitorer un systeme et le
redemarrer en cas de souci, c'est la seule solution en termes de fiabilite
(vu que les composants physiques peuvent claquer, par exemple), mais je vois
trop souvent ca comme une excuse pour ne pas faire programmer correctement.

Par exemple, les souvenir de "bonne pratique" ou on deployait du windows
peu fiable, avec comme consigne de redemarrer tous les trois jours.

Ou les derives actuelles a base de VM, qui sont a mon sens extremement
nocives cote qualite du code.


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

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

Le probleme de l'arret, c'est l'exemple simple qu'on donne aux gens.
Le theoreme suivant dit en gros que les problemes informatiques se separent
en deux categories, les problemes triviaux, et les problemes indecidables
(en nuancant un peu, tu as les problemes triviaux, les NP-complets, et
les indecidables). Une des particularites, c'est que quasiment tout ce qui
est "meta" est indecidable. Dire si un programme s'arrete -> indecidable,
*DIRE SI UN PROGRAMME EST SANS BUG* -> indecidable. Dire si un programme ne
va pas planter pour cause de division par zero -> indecidable.

Pour revenir à ce qui m'intéresse, c'est à dire une spécificité de
l'informatique par rapport aux autres sciences en oeuvre dans les
systèmes industriels, l'informatique est là à égalité avec la
physique et son problème des trois corps (entre autres).

Le rapport avec la programmation reelle ? Il n'y a pratiquement *aucun*
langage industriel qui se preoccupe de ses meta-considerations. Typiquement,
ils sont tous Turing-complets, tout le temps, que tu sois en train de
resoudre des problemes triviaux, ou des problemes impossibles.

Oui et non.
En avionique, on aime bien Lustre/Esterel, qui sont surement Turing complet
(j'ai pas de ref), mais qui ont été pensé pour éviter certains travers
des langages classiques.
Ada, avec ses
for i in tab'range
permettait d'éviter des dépassements de boucle.

Mais ils restent des langages de niche.

Nan, tu as toujours tout, tout le temps. Du coup, on ne peut pas prouver que
les choses marchent, et du coup, on a des bugs.

En physique non plus on a pas trop de moyen de prouver que les choses
marchent, et pourtant, il me paraît plus facile d'y faire des choses robustes.

Evidemment, je suis biaise: je passe beaucoup plus de temps a lire,
a auditer et a corriger du code qu'a en ecrire. Mais pour moi, l'idee
de pouvoir raisonner sur un programme, voire de pouvoir PROUVER des choses
sur celui-ci, c'est quelque chose qui a des TONNES d'applications tres
pratiques et immediates.

Je suis d'accord: plus on saura prouver de choses, plus on chassera de
bugs (à moins que cela rende les programmeurs plus paresseux... "le niveau
baisse", "au temps des cartes perforées, on réflechissait avant d'éxecuter
son code").
Mais c'est la fragilité aux bugs qui me questionne. Un peu comme
si sur un immeuble, un seul caillou dans une pelle de sable pouvait
faire s'écrouler tout l'immeuble.

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

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

Mais c'est la fragilité aux bugs qui me questionne. Un peu comme
si sur un immeuble, un seul caillou dans une pelle de sable pouvait
faire s'écrouler tout l'immeuble.

Si tu fais ton immeuble avec du sable ou même de la terre, tu prends
quand même plus de risque que si tu le construis avec du béton vibré ou
du fer puddlé. Bien sûr, tant le béton comme le fer de construction sont
des inventions récentes, et il semble bien que nous n'avons pas encore
les équivalents informatiques à notre disposition (bien que si l'on
compare au paragraphe précédent, il y a déjà eu des progrès :-))

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


Antoine

Antoine Leca 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

La preuve en physique n'a pas le même statut qu'en mathématique ou en
informatique. La preuve physique n'est juste que de confronter les
prédictions du modèle avec ce qu'on arrive à mesurer. Ca ne prouve pas
que le modèle *est* ce qu'il se passe vraiment. En physique, la réponse
à un pourquoi soulève une question sur un autre pourquoi et ainsi de suite.

Les gens qui utilisent la physique se contentent de l'à-peu-près et
savent vivre avec des phénomènes hautement improbables. Par exemple en
théorie en reliant 2 chambres de pressions différentes, la pression peut
ne pas s'équilibrer, pourtant on fait quand même comme si ca marchait
toujours ainsi. En informatique on ne sait pas encore vraiment vivre et
travailler avec cet à peu-près. Un bon programme est un prog qui marche
à tous les coups dans toutes les situations théoriques. C'est
probablement quelque chose de beaucoup trop strict pour nos besoins
réels, car on devrait pouvoir se contenter, comme en électronique, de
pouvoir utiliser un programme autour de son fonctionnement nominal, dans
une sorte de régime stationnaire.

Je pense aussi comme Marc que cela est lié à la nature des choses
physiques. En fait le nombre d'états internes du programme informatique
(son entropie si cela a du sens) est beaucoup trop petit et cela le rend
sensible à la moindre perturbation. Quand on aura des programmes
informatiques avec beaucoup, mais vraiment beaucoup de bits mis en jeux
et utilisés de façon massivement redondante, alors les programmes seront
probablement beaucoup plus résistants. Autant il existe la physique
statistique, autant il manque une notion de programmation "statistique"
qui reste à définir.

Tiens d'ailleurs il arrive par exemple qu'on double ou triple les
systèmes de décisions avec des algos différents le tout relié à des
algos majoritaires pour avoir un programme qui tolère les fautes. Bon un
facteur X3 c'est pas grand chose, mais c'est déjà un début.

La sécurité viendra probablement plus de systèmes conçus pour être
résistant que de programmes *résistants par construction* ou parce que
le prouveur a dit que c'était ok. En effet, quand bien même le système
formel te prouve que ton algo est 100% correct, il n'aura pas prouvé que
le runtime ou l'OS sont 100% fiables, si même le compilo et le design du
CPU sont sans fautes, ni même que la machine sur laquelle on a compilé
le compilo est sans faute, etc. A ce niveau là la fiabilité est celle du
maillon plus faible de la chaîne et ca peut vite venir sans avoir à
chercher loin. Par exemple ca peut être un simple bit en mémoire qui
vient de lâcher et reste allumé à 1 tout le temps envoyant un prog
prouvé 100% correct dans le décors. Ne l'oublions pas, le hardware est
toujours sujet à panne, mais on ne laisse pas son PC tourner
suffisamment longtemps pour s'en apercevoir et y être sensible.

Quelque part les initiatives telles que Erlang (un truc de Ericsson[*])
sont intéressantes pour ce qui concerne l'écriture de programmes
résistants aux fautes.

http://en.wikipedia.org/wiki/Erlang_%28programming_language%29

sam.
___
[*] Les industriels ne sont pas tous de gros méchants finalement.

Marc Boyer, le 23/06/2010 a écrit :

[...]

Mais ils restent des langages de niche.

Ouah ouah ?

--
Pierre Maurette

Samuel DEVULDER écrivit :

Antoine Leca 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

La preuve en physique n'a pas le même statut qu'en mathématique ou en
informatique.

Oui, je n'étais pas content du tout du mot « preuve » ;
par contre, je n'avais pas compris que le propos de Marc B. fut sur la
définition théorique de la preuve.

La preuve physique n'est juste que de confronter les
prédictions du modèle avec ce qu'on arrive à mesurer.

Par contre, mon idée était de souligner qu'avant Sir Isaac, il n'y avait
pas de modèle du tout, en ce sens que l'on ne pouvait pas faire
d'opérations dessus, tout était pure axiomatique.
Et à mon sens, dans les /systèmes/ informatiques c'est un peu pareil, on
a tout simplement pas de théorie de comment cela fonctionne.

Ca ne prouve pas que le modèle *est* ce qu'il se passe vraiment.

C'est pareil en maths ; regarde la topologie, tu changes quelques
axiomes et le résultat est très différent.
L'amusant avec les maths c'est que comme le système de preuve est très
avancé et très bien maîtrisé, on peut considérer des axiomes aberrants
voire stupides et obtenir quand même des résultats, en physique on ne
peut pas si cela ne s'accorde pas avec le réel observé (comme dans
l'exemple que tu donnes des équilibres de pression).

Un bon programme est un prog qui marche à tous les coups dans toutes
les situations théoriques.

Je ne suis pas d'accord avec cette définition. D'abord parce que si j'ai
bien compris le minimum de théorie (et je parle sous le contrôle de ceux
qui savent, comme les Marc), « marche à tous les coups » n'est pas une
définition opérante (improuvable ? indécidable ?)
Ensuite, parce que cette définition du « bon » est contredite par la
réalité: d'un côté, en tant que technique industrielle (traitement des
données par opposition à la science des ordinateurs, pour reprendre les
termes anglo-saxons), l'informatique est soumis à un impératif
économique qui va changer notablement la notation ; de l'autre, on
trouve des programmes (comme par exemple TeX) qui sont (généralement)
reconnus comme bons, mais qui ne satisfont pas ton critère exhaustif.
Je préfère donc ici le qualificatif de « juste » à la place de « bon ».

La sécurité viendra probablement plus de systèmes conçus pour être
résistant que de programmes *résistants par construction* ou parce que
le prouveur a dit que c'était ok.

C'est effectivement probable, mais la vraie raison est économique : de
la même manière qu'il est plus facile de construire un mur trois fois
plus gros que de calculer les effets de la neige, des tremblements de
terre et autres perturbations sur la structure d'une maison, de même il
paraît plus simple de construire des systèmes redondants que des
systèmes justes : la théorie de la sûreté dit que c'est plus efficace
(et oui, c'est une théorie de type physique, un modèle en accord avec la
réalité observée, pas une démonstration mathématique).

[*] Les industriels ne sont pas tous de gros méchants finalement.

Je ne suis pas gros.


Antoine

In article <hvv4vp$d10$1@shakotay.alphanet.ch>,
Antoine Leca <root@localhost.invalid> wrote:

C'est pareil en maths ; regarde la topologie, tu changes quelques
axiomes et le résultat est très différent.
L'amusant avec les maths c'est que comme le système de preuve est très
avancé et très bien maîtrisé, on peut considérer des axiomes aberrants
voire stupides et obtenir quand même des résultats, en physique on ne
peut pas si cela ne s'accorde pas avec le réel observé (comme dans
l'exemple que tu donnes des équilibres de pression).

Oui et non... tu peux fabriquer toutes les theories que tu veux, du moment
qu'elles sont coherentes. Mais les travaux de Goedel te fournissent les
resultats suivants:
- si une theorie n'est pas coherente (que tu peux prouver que le meme resultat
est vrai ET faux), alors TOUTE la theorie s'ecroule (tu peux prouver tout et
son contraire).
- si une theorie est suffisamment avancee pour contenir l'arithmetique, elle
contient des resultats vrais que tu ne peux pas prouver (e.g., pour lesquels
il est impossible d'ecrire une preuve).
- tu ne peux pas prouver qu'une theorie est coherente (c'est un raisonnement
par l'absurde: si tu arrives a prouver que ta theorie est coherente, alors
ca veut dire qu'elle ne l'est pas !)

Ca fait des fondations assez speciales avec lesquelles on arrive tres bien
a travailler.

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.

Tu peux en general t'en sortir en "bornant tout". 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.

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.

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