On voit souvent des "quel linux choisir ?", des "pourquoi linux ?" etc.
Mais finalement à devoir choisir entre la peste (du côté de chez MS) et
la grippe (notre bon vieux nunux), celà ne vous arrive pas le matin en
vous réveillant de vous dire que les programmes qui font fonctionner
votre machines ne sont que des bidouillages plus ou moins réussis ?
Regardez les codes sources d'un programme en C. Même le code d'un bon
programmeur n'est rempli que d'horreurs. Ce fameux "void" : c'est quoi
cette abomination de la programmation ? Il n'y a aucune sémantique
valable là derrière. D'ailleurs les types en C n'ont de type que le nom.
Comment se fait il qu'on puisse écrire dans la 11e case d'un tableau de
10 éléments. Ce langage surestime beaucoup les capacités des personnes
qui vont l'utiliser. Une telle chose ne doit pas être possible. Comment
imaginer que ce genre de choses peut être voulu par le programmeur ?
Je pense que vous avez déjà vu du JAVA. Mais c'est à gerber cet
emboîtement de new, cette masse colossale de classes à faire pour faire
trois fois rien ! J'ose même pas imaginer la quantité de calculs
inutiles faits par la machine pour gérer ces merdes. D'accord il y a de
l'optimisation, mais c'est loin d'être suffisant.
Dans le temps les programmes étaient bidouillés parce qu'il n'y avait
pas assez de mémoire : par exemple on utilisait une variable pour
stocker deux informations. Maintenant l'horreur est à l'autre extrême :
on a tellement de mémoire de disponible que l'on utilise trop. En C :
tant pis c'est perdu. Un trou de mémoire ? Tant que le pc doit pas
redémarrer toutes les heures à cause de ça on s'en fout. En JAVA : il y
a le ramasse miettes alors on peut bouffer de la mémoire : c'est pô grave.
Dès que les programmes ont commencé à ne plus rentrer sur une disquette
ils sont devenus beaucoup trop compliqués pour fonctionner correctement.
On en vient à une époque où on trouve acceptable un programme quand il a
moins de cent bugs alors que rien que le fait de consommer trop de
ressources fait que le programme n'est pas bon. Aujourd'hui on nous
parle de .NET et de merdouilles dans le genre. A quoi ça sert de se
lancer dans la création de langages qui se copient les uns les autres.
C, C++, JAVA, Pascal : c'est la même chose, la même façon de penser. Et
c'est une manière de penser qui pousse à faire des fautes.
Bref l'informatique ne va pas fort.
Tom , dans le message <422f2d0f$0$27244$, a écrit :
Selon le langage la preuve est plus facile à faire ou pas.
Précisément. Une différence quantitative, pas qualitative.
Une image est une matrice (voire plusieures). Un son est un vecteur si on considère qu'il est digitalisé. Un paquet réseau est un ensemble d'entiers d'un nombre fixé, un type somme en fait. Voilà tout est modélisé. Ca a été dûr.
Tu rigoles j'espère. Pars de la description humainement lisible d'un protocole, disons TCP, et traduis en langage formel ce que ça veut dire. C'est extrêment difficile.
Tom , dans le message <422f2d0f$0$27244$636a15ce@news.free.fr>, a
écrit :
Selon le langage la preuve est plus facile à faire ou pas.
Précisément. Une différence quantitative, pas qualitative.
Une image est une matrice (voire plusieures). Un son est un vecteur si
on considère qu'il est digitalisé. Un paquet réseau est un ensemble
d'entiers d'un nombre fixé, un type somme en fait. Voilà tout est
modélisé. Ca a été dûr.
Tu rigoles j'espère. Pars de la description humainement lisible d'un
protocole, disons TCP, et traduis en langage formel ce que ça veut dire.
C'est extrêment difficile.
Tom , dans le message <422f2d0f$0$27244$, a écrit :
Selon le langage la preuve est plus facile à faire ou pas.
Précisément. Une différence quantitative, pas qualitative.
Une image est une matrice (voire plusieures). Un son est un vecteur si on considère qu'il est digitalisé. Un paquet réseau est un ensemble d'entiers d'un nombre fixé, un type somme en fait. Voilà tout est modélisé. Ca a été dûr.
Tu rigoles j'espère. Pars de la description humainement lisible d'un protocole, disons TCP, et traduis en langage formel ce que ça veut dire. C'est extrêment difficile.
Nicolas George
Richard Delorme , dans le message <422f3453$0$17033$, a écrit :
(c n'est pas une lvalue).
<tetratomie>
Si, d'ailleurs on peut légalement écrire &c.
</tetratomie>
Richard Delorme , dans le message
<422f3453$0$17033$7a628cd7@news.club-internet.fr>, a écrit :
Richard Delorme , dans le message <422f3453$0$17033$, a écrit :
(c n'est pas une lvalue).
<tetratomie>
Si, d'ailleurs on peut légalement écrire &c.
</tetratomie>
Nicolas George
Joe Cool , dans le message <422f3883$0$15677$, a écrit :
Vous avez beau critiquer la mienne (en fait vous la rejettez sans justification), au moins elle veut dire quelque chose.
Elle veut dire quelque chose qui n'est pas une notion intéressante. Savoir ce qui est intéressant ou pas comme notion n'est pas justifiable rigoureusement, mais on peut le voir en pratique. Ta définition de portabilité donne un thread ou deux gus se ridiculisent sur fcold. « Ma » définition de portabilité donne un noyau Linux qui tourne sur vingt architectures différentes en tirant partie de leurs performances. C'est vite vu.
Joe Cool , dans le message <422f3883$0$15677$626a14ce@news.free.fr>, a
écrit :
Vous avez
beau critiquer la mienne (en fait vous la rejettez sans justification),
au moins elle veut dire quelque chose.
Elle veut dire quelque chose qui n'est pas une notion intéressante. Savoir
ce qui est intéressant ou pas comme notion n'est pas justifiable
rigoureusement, mais on peut le voir en pratique. Ta définition de
portabilité donne un thread ou deux gus se ridiculisent sur fcold. « Ma »
définition de portabilité donne un noyau Linux qui tourne sur vingt
architectures différentes en tirant partie de leurs performances. C'est vite
vu.
Joe Cool , dans le message <422f3883$0$15677$, a écrit :
Vous avez beau critiquer la mienne (en fait vous la rejettez sans justification), au moins elle veut dire quelque chose.
Elle veut dire quelque chose qui n'est pas une notion intéressante. Savoir ce qui est intéressant ou pas comme notion n'est pas justifiable rigoureusement, mais on peut le voir en pratique. Ta définition de portabilité donne un thread ou deux gus se ridiculisent sur fcold. « Ma » définition de portabilité donne un noyau Linux qui tourne sur vingt architectures différentes en tirant partie de leurs performances. C'est vite vu.
Nicolas George
JustMe , dans le message , a écrit :
Donc la "Preuve Mathématique" n'est pas forcément possible
Oui.
Ce qui doit etre prouvé c'est la proposition "Le programme correspond exactement au but X" Le fait que X existe ne rend pas la proposition en question décidable pour autant.
Effectivement. Mais justement, si tu n'arrives pas à prouver que ton programme marche, c'est _probablement_ parce qu'il ne marche pas. Quand tu écris le programme, tu l'écris pour qu'il marche, ce qui signifie que tu as une vue intuitive des grandes lignes de la preuve. C'est donc se placer _a priori_ dans un cas qui est décidable.
D'autant que X n'est pas forcément correctement defini. Mais là c'est un autre probleme... ;-)
Tout à fait.
JustMe , dans le message <mn.4c5e7d53db902913.15643@merci.beaucoup>, a
écrit :
Donc la "Preuve Mathématique" n'est pas forcément possible
Oui.
Ce qui doit etre prouvé c'est la proposition "Le programme correspond
exactement au but X"
Le fait que X existe ne rend pas la proposition en question décidable
pour autant.
Effectivement. Mais justement, si tu n'arrives pas à prouver que ton
programme marche, c'est _probablement_ parce qu'il ne marche pas. Quand tu
écris le programme, tu l'écris pour qu'il marche, ce qui signifie que tu as
une vue intuitive des grandes lignes de la preuve. C'est donc se placer _a
priori_ dans un cas qui est décidable.
D'autant que X n'est pas forcément correctement defini. Mais là c'est
un autre probleme... ;-)
Donc la "Preuve Mathématique" n'est pas forcément possible
Oui.
Ce qui doit etre prouvé c'est la proposition "Le programme correspond exactement au but X" Le fait que X existe ne rend pas la proposition en question décidable pour autant.
Effectivement. Mais justement, si tu n'arrives pas à prouver que ton programme marche, c'est _probablement_ parce qu'il ne marche pas. Quand tu écris le programme, tu l'écris pour qu'il marche, ce qui signifie que tu as une vue intuitive des grandes lignes de la preuve. C'est donc se placer _a priori_ dans un cas qui est décidable.
D'autant que X n'est pas forcément correctement defini. Mais là c'est un autre probleme... ;-)
Tout à fait.
Joe Cool
Joe Cool , dans le message <422f2845$0$18054$, a
Je suis désolé mais cette erreur vient de votre système.
Non, cette erreur est tout à fait normale, c'est juste toi qui dis des conneries sur Caml comme sur le C.
Je voudrais bien savoir pourquoi ce programme qui est sensé planter me renvoie une gentille exception Stack_overflow aussi bien en version code-octet qu'en version native.
-- Joe Cool
Joe Cool , dans le message <422f2845$0$18054$636a15ce@news.free.fr>, a
Je suis désolé mais cette erreur vient de votre système.
Non, cette erreur est tout à fait normale, c'est juste toi qui dis des
conneries sur Caml comme sur le C.
Je voudrais bien savoir pourquoi ce programme qui est sensé planter me
renvoie une gentille exception Stack_overflow aussi bien en version
code-octet qu'en version native.
Je suis désolé mais cette erreur vient de votre système.
Non, cette erreur est tout à fait normale, c'est juste toi qui dis des conneries sur Caml comme sur le C.
Je voudrais bien savoir pourquoi ce programme qui est sensé planter me renvoie une gentille exception Stack_overflow aussi bien en version code-octet qu'en version native.
-- Joe Cool
Joe Cool
Bien sûr, une preuve ça ne sert à rien.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur les 8 premiers entiers, c'est bien suffisant.
1 est premier
Ah bon ?
Oui, car il n'est divisible que par 1 et par lui même.
-- Joe Cool
Bien sûr, une preuve ça ne sert à rien.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me
fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur
les 8 premiers entiers, c'est bien suffisant.
1 est premier
Ah bon ?
Oui, car il n'est divisible que par 1 et par lui même.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur les 8 premiers entiers, c'est bien suffisant.
1 est premier
Ah bon ?
Oui, car il n'est divisible que par 1 et par lui même.
-- Joe Cool
Eric Jacoboni
Nicolas George <nicolas$ writes:
(c n'est pas une lvalue).
<tetratomie>
Si, d'ailleurs on peut légalement écrire &c.
</tetratomie>
On va dire que ce n'est pas une lvalue modifiable, alors...
-- Éric Jacoboni, né il y a 1413832428 secondes
Nicolas George <nicolas$george@salle-s.org> writes:
(c n'est pas une lvalue).
<tetratomie>
Si, d'ailleurs on peut légalement écrire &c.
</tetratomie>
On va dire que ce n'est pas une lvalue modifiable, alors...
On va dire que ce n'est pas une lvalue modifiable, alors...
-- Éric Jacoboni, né il y a 1413832428 secondes
Joe Cool
Joe Cool , dans le message <422f1ee4$0$31419$, a
Non car le système de type du C est incohérent. Le système de typage de caml génère pour chaque programme la preuve qu'il utilise ses données de manière cohérente
Or comme cette preuve est indécidable, le langage Caml restreint considérablement ce qu'il est autorisé d'écrire pour forcer le programmeur à rester dans les cas que sait traiter le compilateur. Ça fait une limitation d'expressivité extrêmement forte. À tel point, d'ailleurs, qu'il y a à plusieurs endroits de la bibliothèque standard de Caml des usages de Obj.magic pour contourner la limitation.
Ce n'est pas bien de contourner le système de type. Dans ce cas, autant ne rien typer.
-- Joe Cool
Joe Cool , dans le message <422f1ee4$0$31419$636a15ce@news.free.fr>, a
Non car le système de type du C est incohérent. Le système de typage de
caml génère pour chaque programme la preuve qu'il utilise ses données de
manière cohérente
Or comme cette preuve est indécidable, le langage Caml restreint
considérablement ce qu'il est autorisé d'écrire pour forcer le programmeur à
rester dans les cas que sait traiter le compilateur. Ça fait une limitation
d'expressivité extrêmement forte. À tel point, d'ailleurs, qu'il y a à
plusieurs endroits de la bibliothèque standard de Caml des usages de
Obj.magic pour contourner la limitation.
Ce n'est pas bien de contourner le système de type. Dans ce cas, autant
ne rien typer.
Non car le système de type du C est incohérent. Le système de typage de caml génère pour chaque programme la preuve qu'il utilise ses données de manière cohérente
Or comme cette preuve est indécidable, le langage Caml restreint considérablement ce qu'il est autorisé d'écrire pour forcer le programmeur à rester dans les cas que sait traiter le compilateur. Ça fait une limitation d'expressivité extrêmement forte. À tel point, d'ailleurs, qu'il y a à plusieurs endroits de la bibliothèque standard de Caml des usages de Obj.magic pour contourner la limitation.
Ce n'est pas bien de contourner le système de type. Dans ce cas, autant ne rien typer.
-- Joe Cool
Richard Delorme
Un typage *est* une preuve.
Qui ne sert à rien. Lire p.ex. : http://mindview.net/WebLog/log-0025 « In fact, what we need is
*Strong testing, not strong typing.* »
Bien sûr, une preuve ça ne sert à rien.
En pratique, ça sert peu.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur les 8 premiers entiers, c'est bien suffisant.
1 est premier
Non, 1 n'est pas premier, et il manque 2 qui est premier.
3 est premier 5 est premier 7 est premier donc tous les entiers impairs sont premiers
Bon exemple. Sur les 8 premiers entiers, 3 sont impairs et 1 autre est pair, donc on n'en conclut rien du tout. Ici, le test suffit, pas besoin de s'embêter avec un truc plus compliqué.
-- Richard
Un typage *est* une preuve.
Qui ne sert à rien. Lire p.ex. :
http://mindview.net/WebLog/log-0025
« In fact, what we need is
*Strong testing, not strong typing.*
»
Bien sûr, une preuve ça ne sert à rien.
En pratique, ça sert peu.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me
fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur
les 8 premiers entiers, c'est bien suffisant.
1 est premier
Non, 1 n'est pas premier, et il manque 2 qui est premier.
3 est premier
5 est premier
7 est premier
donc tous les entiers impairs sont premiers
Bon exemple. Sur les 8 premiers entiers, 3 sont impairs et 1 autre est
pair, donc on n'en conclut rien du tout. Ici, le test suffit, pas besoin
de s'embêter avec un truc plus compliqué.
Qui ne sert à rien. Lire p.ex. : http://mindview.net/WebLog/log-0025 « In fact, what we need is
*Strong testing, not strong typing.* »
Bien sûr, une preuve ça ne sert à rien.
En pratique, ça sert peu.
Quand je doit démontrer un truc sur les entiers, je me dis à quoi bon me fatiquer à faire une preuve qui ne sert à rien : je vais la tester sur les 8 premiers entiers, c'est bien suffisant.
1 est premier
Non, 1 n'est pas premier, et il manque 2 qui est premier.
3 est premier 5 est premier 7 est premier donc tous les entiers impairs sont premiers
Bon exemple. Sur les 8 premiers entiers, 3 sont impairs et 1 autre est pair, donc on n'en conclut rien du tout. Ici, le test suffit, pas besoin de s'embêter avec un truc plus compliqué.
-- Richard
Joe Cool
Joe Cool , dans le message <422f210e$0$31419$, a
La détection des fuites de mémoire l'est peut être, mais la prévention des fuites est on ne peut plus décidable. On appelle ça des ramasse-miettes.
Oui, et ça a un coût très important en efficacité, surtout au moment où la mémoire utilisée par le programme dépasse la mémoire physique de l'hôte. Dès lors, permettre une gestion plus fine, mais non décidable par le compilateur, est indispensable.
Le coût est amorti, ce qui occasionne un ralentissement négligeable. En tout cas ça a l'air de bien marcher en pratique.
-- Joe Cool
Joe Cool , dans le message <422f210e$0$31419$636a15ce@news.free.fr>, a
La détection des fuites de mémoire l'est peut être, mais la prévention
des fuites est on ne peut plus décidable. On appelle ça des ramasse-miettes.
Oui, et ça a un coût très important en efficacité, surtout au moment où la
mémoire utilisée par le programme dépasse la mémoire physique de l'hôte. Dès
lors, permettre une gestion plus fine, mais non décidable par le
compilateur, est indispensable.
Le coût est amorti, ce qui occasionne un ralentissement négligeable. En
tout cas ça a l'air de bien marcher en pratique.
La détection des fuites de mémoire l'est peut être, mais la prévention des fuites est on ne peut plus décidable. On appelle ça des ramasse-miettes.
Oui, et ça a un coût très important en efficacité, surtout au moment où la mémoire utilisée par le programme dépasse la mémoire physique de l'hôte. Dès lors, permettre une gestion plus fine, mais non décidable par le compilateur, est indispensable.
Le coût est amorti, ce qui occasionne un ralentissement négligeable. En tout cas ça a l'air de bien marcher en pratique.
