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.
C'est justement parce que quelqu'un a dit "ADA, c'est moisi", que le problème a surgi. Dépassement de capacité dans un registre, ADA travaillant sur 6 bits, le C sur 8 et boum... Le C ne sait pas gérer une exception...
Ils ont tenté avec le C++. Mais va dire à des gens qui font des if ((machin = bidule()) == 0) que ce n'est pas gérer des erreurs correctement. Surtout que parfois c'est 0 parfois -1, etc.
Tom
C'est justement parce que quelqu'un a dit "ADA, c'est moisi", que le
problème a surgi. Dépassement de capacité dans un registre, ADA
travaillant sur 6 bits, le C sur 8 et boum... Le C ne sait pas
gérer une exception...
Ils ont tenté avec le C++. Mais va dire à des gens qui font des
if ((machin = bidule()) == 0)
que ce n'est pas gérer des erreurs correctement. Surtout que parfois
c'est 0 parfois -1, etc.
C'est justement parce que quelqu'un a dit "ADA, c'est moisi", que le problème a surgi. Dépassement de capacité dans un registre, ADA travaillant sur 6 bits, le C sur 8 et boum... Le C ne sait pas gérer une exception...
Ils ont tenté avec le C++. Mais va dire à des gens qui font des if ((machin = bidule()) == 0) que ce n'est pas gérer des erreurs correctement. Surtout que parfois c'est 0 parfois -1, etc.
Tom
Joe Cool
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un programme qui serve vraiment à quelque chose dans la vraie vie (un traitement de texte, un navigateur web, un serveur de news, un système de comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
-- Joe Cool
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un
programme qui serve vraiment à quelque chose dans la vraie vie (un
traitement de texte, un navigateur web, un serveur de news, un système de
comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un programme qui serve vraiment à quelque chose dans la vraie vie (un traitement de texte, un navigateur web, un serveur de news, un système de comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
-- Joe Cool
Joe Cool
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.
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 3 est premier 5 est premier 7 est premier donc tous les entiers impairs sont premiers
-- Joe Cool
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.
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
3 est premier
5 est premier
7 est premier
donc tous les entiers impairs sont premiers
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.
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 3 est premier 5 est premier 7 est premier donc tous les entiers impairs sont premiers
-- Joe Cool
JustMe
Joe Cool avait énoncé :
Et dérécursiver ca n'est pas modifier un comportement ? lol
Non, car ça ne modifie pas la complexité, ni la sémantique du calcul.
Ah ?
mmm....
Joe Cool avait énoncé :
Et dérécursiver ca n'est pas modifier un comportement ? lol
Non, car ça ne modifie pas la complexité, ni la sémantique du calcul.
Et dérécursiver ca n'est pas modifier un comportement ? lol
Non, car ça ne modifie pas la complexité, ni la sémantique du calcul.
Ah ?
mmm....
Tom
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.* » Donc ce Bruce Eckel c'est *LA* référence si j'ai bien compris. Un seul
blanc bec se pointe comme ça (avec des exemple en Java, j'apprécie) et piétine les travaux sur les lambda-calculs typés. Non mais faut vérifier ses sources parfois.
Cherche "isomorphisme de Curry-Howard" sur Google. C'est très instructif. Si tu as des notions de lambda-calcul tu verras que le type d'un terme (donc d'un programme) est une preuve mathématique. Un programme correctement typé correspond à une preuve. Ca ne vérifie pas forcément la spécification, mais au moins que ce qui est écrit est un programme, ce qui élimine beaucoup d'erreurs.
Tom
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.*
»
Donc ce Bruce Eckel c'est *LA* référence si j'ai bien compris. Un seul
blanc bec se pointe comme ça (avec des exemple en Java, j'apprécie) et
piétine les travaux sur les lambda-calculs typés. Non mais faut vérifier
ses sources parfois.
Cherche "isomorphisme de Curry-Howard" sur Google. C'est très
instructif. Si tu as des notions de lambda-calcul tu verras que le type
d'un terme (donc d'un programme) est une preuve mathématique. Un
programme correctement typé correspond à une preuve.
Ca ne vérifie pas forcément la spécification, mais au moins que ce qui
est écrit est un programme, ce qui élimine beaucoup d'erreurs.
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.* » Donc ce Bruce Eckel c'est *LA* référence si j'ai bien compris. Un seul
blanc bec se pointe comme ça (avec des exemple en Java, j'apprécie) et piétine les travaux sur les lambda-calculs typés. Non mais faut vérifier ses sources parfois.
Cherche "isomorphisme de Curry-Howard" sur Google. C'est très instructif. Si tu as des notions de lambda-calcul tu verras que le type d'un terme (donc d'un programme) est une preuve mathématique. Un programme correctement typé correspond à une preuve. Ca ne vérifie pas forcément la spécification, mais au moins que ce qui est écrit est un programme, ce qui élimine beaucoup d'erreurs.
Tom
JKB
Le 09-03-2005, à propos de Re: a-t-on le choix ?, Tom écrivait dans fr.comp.os.linux.debats :
http://www.systella.fr/~bertrand/freevms
Je met la bonne adresse, pour ceux qui s'arrêteront à la page 404 pointée par le précédent lien. Perso je testerais bien mais je n'ai pas de VAX sous la main.
Merci de corriger. Ça fonctionne sous x86. Tous les contributeurs sont les bienvenus.
JKB
Le 09-03-2005, à propos de
Re: a-t-on le choix ?,
Tom écrivait dans fr.comp.os.linux.debats :
http://www.systella.fr/~bertrand/freevms
Je met la bonne adresse, pour ceux qui s'arrêteront à la page 404
pointée par le précédent lien. Perso je testerais bien mais je n'ai pas
de VAX sous la main.
Le 09-03-2005, à propos de Re: a-t-on le choix ?, Tom écrivait dans fr.comp.os.linux.debats :
http://www.systella.fr/~bertrand/freevms
Je met la bonne adresse, pour ceux qui s'arrêteront à la page 404 pointée par le précédent lien. Perso je testerais bien mais je n'ai pas de VAX sous la main.
Merci de corriger. Ça fonctionne sous x86. Tous les contributeurs sont les bienvenus.
JKB
Joe Cool
Un typage est dit statique quand le type des données est décidé au moment de la compilation.
Et donc ? En C, c'est encore mieux, le type des données est décidé *avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu n'aurais pas compris) ?
La machine vérifie le type et le devine en observant la manière dont le programme utilise ses données. On évite les erreurs de typage dues au programmeur et on certifie que le programme ne peut en aucun cas générer d'erreur d'exécution : un programme typé statiquement ne peut pas planter.
Un typage *est* une preuve.
Preuve de quoi ? De la cohérence des types ? De la correction du programme (ce qui est en générale ce qu'on appelle preuve, et qui est très difficile à faire automatiquement puisque la machine est incapable de deviner ce qu'on veut faire, et à même beaucoup de mal à comprendre quand on lui explique), certainement pas. En même temps, ça m'arrangerait, comme tout mes programmes C sont correctement typés, ça prouverait qu'ils sont corrects.
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 : il génère la preuve que le programme ne peut pas planter. Du moins si il plante, ce n'est pas de sa faute mais celle du système d'exploitation ou du matériel.
Alors quand tu racontes ce genre de choses, tu m'excuseras, mais tu me fais doucement rigoler. Je pense que la seule chose que tu prouves c'est que tu ne sais pas (mais alors vraiment pas) du tout de quoi tu parles.
Ignorance, quand tu nous tiens.
Tu parles pour toi ?
Non, je parle pour quelqu'un d'autre.
-- Joe Cool
Un typage est dit statique quand le type des données est décidé au
moment de la compilation.
Et donc ? En C, c'est encore mieux, le type des données est décidé
*avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on
manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu
n'aurais pas compris) ?
La machine vérifie le type et le devine en observant la manière dont le
programme utilise ses données. On évite les erreurs de typage dues au
programmeur et on certifie que le programme ne peut en aucun cas générer
d'erreur d'exécution : un programme typé statiquement ne peut pas planter.
Un typage *est* une preuve.
Preuve de quoi ? De la cohérence des types ? De la correction du
programme (ce qui est en générale ce qu'on appelle preuve, et qui est
très difficile à faire automatiquement puisque la machine est incapable
de deviner ce qu'on veut faire, et à même beaucoup de mal à comprendre
quand on lui explique), certainement pas. En même temps, ça
m'arrangerait, comme tout mes programmes C sont correctement typés, ça
prouverait qu'ils sont corrects.
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 : il génère la preuve que le programme ne peut pas
planter. Du moins si il plante, ce n'est pas de sa faute mais celle du
système d'exploitation ou du matériel.
Alors quand tu racontes ce genre de choses, tu m'excuseras,
mais tu me fais doucement rigoler. Je pense que la seule chose que tu
prouves c'est que tu ne sais pas (mais alors vraiment pas) du tout de
quoi tu parles.
Un typage est dit statique quand le type des données est décidé au moment de la compilation.
Et donc ? En C, c'est encore mieux, le type des données est décidé *avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu n'aurais pas compris) ?
La machine vérifie le type et le devine en observant la manière dont le programme utilise ses données. On évite les erreurs de typage dues au programmeur et on certifie que le programme ne peut en aucun cas générer d'erreur d'exécution : un programme typé statiquement ne peut pas planter.
Un typage *est* une preuve.
Preuve de quoi ? De la cohérence des types ? De la correction du programme (ce qui est en générale ce qu'on appelle preuve, et qui est très difficile à faire automatiquement puisque la machine est incapable de deviner ce qu'on veut faire, et à même beaucoup de mal à comprendre quand on lui explique), certainement pas. En même temps, ça m'arrangerait, comme tout mes programmes C sont correctement typés, ça prouverait qu'ils sont corrects.
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 : il génère la preuve que le programme ne peut pas planter. Du moins si il plante, ce n'est pas de sa faute mais celle du système d'exploitation ou du matériel.
Alors quand tu racontes ce genre de choses, tu m'excuseras, mais tu me fais doucement rigoler. Je pense que la seule chose que tu prouves c'est que tu ne sais pas (mais alors vraiment pas) du tout de quoi tu parles.
Ignorance, quand tu nous tiens.
Tu parles pour toi ?
Non, je parle pour quelqu'un d'autre.
-- Joe Cool
Tom
Et donc ? En C, c'est encore mieux, le type des données est décidé *avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu n'aurais pas compris) ?
Il n'y a pas de types en C bon sang ! Un char, un int, un void c'est la même chose. Quand il n'y a qu'un type c'est qu'il n'y a pas de type.
Tiens, c'est vrai. Apparemment au prix de certaines contorsions. Bon, passons. Vu mon expérience de la programmation objet, j'aurais pu me passer de donner un exemple pareil.
Les objets sont des abominations. L'objet est une extension propre à Objective Caml en ce qui concerne Caml.
En même temps, ça m'arrangerait, comme tout mes programmes C sont correctement typés, ça prouverait qu'ils sont corrects.
Ils ne sont pas typés. n-ième édition.
Tu parles pour toi ?
Ca c'est de l'argument. Je vais essayer de me rappeler de ce que je dissais à la maternelle dans de telles situations.
Tom
Et donc ? En C, c'est encore mieux, le type des données est décidé
*avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on
manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu
n'aurais pas compris) ?
Il n'y a pas de types en C bon sang ! Un char, un int, un void c'est la
même chose. Quand il n'y a qu'un type c'est qu'il n'y a pas de type.
Tiens, c'est vrai. Apparemment au prix de certaines contorsions. Bon,
passons. Vu mon expérience de la programmation objet, j'aurais pu me
passer de donner un exemple pareil.
Les objets sont des abominations. L'objet est une extension propre à
Objective Caml en ce qui concerne Caml.
En même temps, ça m'arrangerait, comme tout mes programmes C sont
correctement typés, ça prouverait qu'ils sont corrects.
Ils ne sont pas typés. n-ième édition.
Tu parles pour toi ?
Ca c'est de l'argument. Je vais essayer de me rappeler de ce que je
dissais à la maternelle dans de telles situations.
Et donc ? En C, c'est encore mieux, le type des données est décidé *avant* la compilation, ce qui, du reste, permet de comprendre ce qu'on manipule. En quoi est-ce un avantage (c'était ma question, au cas où tu n'aurais pas compris) ?
Il n'y a pas de types en C bon sang ! Un char, un int, un void c'est la même chose. Quand il n'y a qu'un type c'est qu'il n'y a pas de type.
Tiens, c'est vrai. Apparemment au prix de certaines contorsions. Bon, passons. Vu mon expérience de la programmation objet, j'aurais pu me passer de donner un exemple pareil.
Les objets sont des abominations. L'objet est une extension propre à Objective Caml en ce qui concerne Caml.
En même temps, ça m'arrangerait, comme tout mes programmes C sont correctement typés, ça prouverait qu'ils sont corrects.
Ils ne sont pas typés. n-ième édition.
Tu parles pour toi ?
Ca c'est de l'argument. Je vais essayer de me rappeler de ce que je dissais à la maternelle dans de telles situations.
Tom
JustMe
Joe Cool avait écrit le 09/03/2005 :
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un programme qui serve vraiment à quelque chose dans la vraie vie (un traitement de texte, un navigateur web, un serveur de news, un système de comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
Vous confondez "défis" et "attaque".
Joe Cool avait écrit le 09/03/2005 :
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un
programme qui serve vraiment à quelque chose dans la vraie vie (un
traitement de texte, un navigateur web, un serveur de news, un système de
comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
Eh bien vas-y, montre-nous comme tu es fort : choisis ton langage, fais un programme qui serve vraiment à quelque chose dans la vraie vie (un traitement de texte, un navigateur web, un serveur de news, un système de comptabilité), et prouve qu'il fonctionne.
On va bien rire, tiens.
Les attaques ad hominem commencent à pulluler. Ce n'est pas sérieux.
Vous confondez "défis" et "attaque".
Tom
Oui, et? Tu compares Dijkstra à Einstein?
Dijkstra est l'un des plus grands informaticiens ayant existé. Et je ne vois pas pourquoi on devrait comparer Dijkstra à Einstein. Ils ne travaillaient pas dans le même domaine.
Tom
Oui, et? Tu compares Dijkstra à Einstein?
Dijkstra est l'un des plus grands informaticiens ayant existé. Et je ne
vois pas pourquoi on devrait comparer Dijkstra à Einstein. Ils ne
travaillaient pas dans le même domaine.
Dijkstra est l'un des plus grands informaticiens ayant existé. Et je ne vois pas pourquoi on devrait comparer Dijkstra à Einstein. Ils ne travaillaient pas dans le même domaine.
