EDForum :: Voir le sujet - Shoot-First Law

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 30 Sep 2005 23:24

[EDIT de Darathor : topic extrait de là]

Rupert a écrit :

Citation :
Je me basait sur une logique non-booléaine ou non True est différent de False.

Faut le faire pour sortir tant de conneries dans DG

Fait gaffe où je te fais un cours sur cela avec un bonus une méthode d'implémentation de classe pour Hava et de Type pour OCaml

| Profil | MP | Site web

Rupert

Modérateur
Fils de Chuck Norris

Inscrit le : 23 Juil 2003
Messages : 35683
Points : 60 Concours jeux - 20e place

378

Concours graphiques - Médaille d'or : première place

Séries favorites : BTVS - Friends

Posté le : 30 Sep 2005 23:31

T'es gentil, mais je m'en suis suffisemment tapé de cours sur ces conneries inutiles :we:

D'ailleurs, je sais pas comment tu fais pour en parler dans ce topic :we:

vive toi tiens

hum hum, on est HS

_________________

| Profil | MP | E-mail | Site web

MeRyL

Maîtresse des Arcanes

Inscrit le : 20 Fév 2003
Messages : 8641
Points : 3 Concours jeux - 43e place

195

Séries favorites : Btvs - Stargate SG1 - Lost

Posté le : 01 Oct 2005 00:00

WTF ?

| Profil | MP

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 00:04

Rupert a écrit :

T'es gentil, mais je m'en suis suffisemment tapé de cours sur ces conneries inutiles

La logique c'est pas inutile¹

Ça manque un peu à pas mal de gens d'ailleurs

Cela dit, on écrit "booléen" et "booléenne", pas de "ai" là dedans

_________________
¹ : Caml, par contre, ça c'est inutile :we:

_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web

Dernière édition par Darathor le 01 Oct 2005 00:06; édité 3 fois

Z

Archimage

Inscrit le : 06 Juin 2003
Messages : 12130
Points : 75 Concours jeux - 12e place

81

Séries favorites : Little House on the Prairie, The Bold & The Beautiful

Posté le : 01 Oct 2005 00:04

rien capté :gni:

| Profil | MP

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 00:10

Darathor a écrit :

Caml, par contre, ça c'est inutile

Bof, le seul langage de programmation où on peut démontrer que le code est bon, avec un algorithme d'inférence de type absolument génial et capable de générer lui même un code optimisé à partir de l'algorithme... Sans oublier un des lanngages de programmaion les plus performants, et le plus performant parmi ceux de haut niveau...

| Profil | MP | Site web

Rupert

Modérateur
Fils de Chuck Norris

Inscrit le : 23 Juil 2003
Messages : 35683
Points : 60 Concours jeux - 20e place

378

Séries favorites : BTVS - Friends

Posté le : 01 Oct 2005 00:12

Dit, cette manière ridicule de parler, c'est pour faire style ou c'est de l'humour? :we:

Dans les deux cas, je suis pas réceptif

_________________

| Profil | MP | E-mail | Site web

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 00:13

N'empêche que :
1) Il est chiant à utiliser.
2) Les prouveurs finiront bien par produire autre chose que du fonctionnel, genre du Java

3) À part dans les labos de recherhce, il n'est utilisé grosso-modo nul part... Donc l'apprendre, à moins de se destiner à la recherche ne sert pas à grand chose, si ce n'est avoir vu un jour un langage fonctionnel, ce qui en théorie peut bien servir un jour, on sait jamais... Mais y a peu de chances quand même...

EDIT : Cela dit, on vire vaguement HS là :-D

_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web

Dernière édition par Darathor le 01 Oct 2005 00:16; édité 1 fois

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 00:14

Rupert a écrit :

Dans les deux cas, je suis pas réceptif

T'as pas l'air receptif a beaucoup de trucs en même temps.... :nonnon:

| Profil | MP | Site web

MeRyL

Maîtresse des Arcanes

Inscrit le : 20 Fév 2003
Messages : 8641
Points : 3 Concours jeux - 43e place

195

Séries favorites : Btvs - Stargate SG1 - Lost

Posté le : 01 Oct 2005 00:14

En tout cas sa marche, je vais aller me coucher en me pensant totalement ignorante sur les realités de ce monde :peur2:

[Rupy, ta sign est M.a.g.n.i.f.i.q.u.e :tourni:

]

| Profil | MP

Z

Archimage

Inscrit le : 06 Juin 2003
Messages : 12130
Points : 75 Concours jeux - 12e place

81

Séries favorites : Little House on the Prairie, The Bold & The Beautiful

Posté le : 01 Oct 2005 00:15

Lumen a écrit :

Rupert a écrit :

Dans les deux cas, je suis pas réceptif

T'as pas l'air receptif a beaucoup de trucs en même temps....

Euh faut pas jeter mémé dans les orties non plus, t'as vu comme tu parles :blase:

!!!

| Profil | MP

Rupert

Modérateur
Fils de Chuck Norris

Inscrit le : 23 Juil 2003
Messages : 35683
Points : 60 Concours jeux - 20e place

378

Séries favorites : BTVS - Friends

Posté le : 01 Oct 2005 00:16

Je plussoie Meryl, je me sens tout idiot :peur2:

Flûte alors :peur2:

et merci au passage :razz:

C'est tout HS là :peur2:

_________________

| Profil | MP | E-mail | Site web

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 00:20

Darathor a écrit :

N'empêche que :
1) Il est chiant à utiliser.
2) Les prouveurs finiront bien par produire autre chose que du fonctionnel, genre du Java
3) À part dans les labos de recherhce, il n'est utilisé grosso-modo nul part... Donc l'apprendre, à moins de se destiner à la recherche ne sert pas à grand chose, si ce n'est avoir vu un jour un langage fonctionnel, ce qui en théorie peut bien servir un jour, on sait jamais... Mais y a peu de chances quand même...

1) Non, il respecte un esprit mathématique assez clair
2) Peu de chance que ce soit faisable en objet. L'inférence de type y est quasiment impossible et la surcharge obligatoire si on ne veut pas tomber dans les travers du Java, justement, qui est un langage gourmand et sale... Le fonctionnel et peut être l'impératif (Ada avait été pas mal à ce sujet) sont les plus gros prétendants actuels
3) Caml et Ada sont utilisés comme base pour créer des langages spécifiques dans des applications nécéssitant une sécurité abolu. La dernière ligne de métro par exemple, est automatisé en partie avec ces deux langages.

Tout ça pour dire que rien n'est tout noir, rien n'est tout blanc, le gris existe! Démonstration trouvable en 15 pages demain

| Profil | MP | Site web

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 00:31

Ben d'après le prof qui nous faisait le cours de Coq (un prouveur qui ne produit que du CAML pour l'instant) disait que la production de C et Java était en cours de développement... Comme quoi...

Et le prof de GL (intervenant extérieur bossant dans une boîte de développement de systèmes critiques et ayant entre autre produit du code pour airbus et si je me souviens bien également pour un satellite) semblait utiliser de l'objet également vu que tout son cours sur leur méthode de développement se basait sur la modélisation en objets (avec UML) :ack:

_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 08:27

Pour le C, je suis au courant. Mais ça va être dur car un même code source pourra réagir differement selon le compilateur et l'OS... DOnc à moins de nettoyer le langage, ça ne sra pas possible.

Pour le Java... Autant partir du C# plutôt. Le gros inconvénient du Java est qu'il est extremement gourmand et permet des manipulations assez sales. On peut faire boucler du Java sans utiliser de structures pour, et tant que ça sera le cas, on ne pourra rien prouver avec, vu qu'un programme dépourvu de boucles pourra ne pas terminer.

Par contre, pour ce qui est de la programmation dans l'aéronotique, c'est direct en assembleur. La modélisation oeut ne pas correspondre au type de langage emplyé. Pour ce qui est de l'infographie par exemple, on utilise généralement des langages impératifs avec une modélisation objet. Et la manière de programmé ressemblera à de l'objet, mais dans un langage impératif.
Il ne faut pas oublier quà la fiin, on a de l'assembleur, qui est un langage impératif de très bas niveau. Mais la structure du code pourra être modélisé en objet

| Profil | MP | Site web

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 11:43

Lumen a écrit :

Pour le Java... Autant partir du C# plutôt. Le gros inconvénient du Java est qu'il est extremement gourmand et permet des manipulations assez sales. On peut faire boucler du Java sans utiliser de structures pour, et tant que ça sera le cas, on ne pourra rien prouver avec, vu qu'un programme dépourvu de boucles pourra ne pas terminer.

C'est pas parce qu'on permet des trucs pas propre dans le langage en général qu'on ne peut pas prouver un programme... De base je vois pas où c'est contradictoire...

Lumen a écrit :

Par contre, pour ce qui est de la programmation dans l'aéronotique, c'est direct en assembleur.

À la limite ils refont en assembleur pour l'optimiser mais ça m'étonnerait très franchement qu'ils développent direct en assembleur (à part quelques petites portions)... Donc le langage de haut niveau sert quand même largement plus.

Lumen a écrit :

La modélisation oeut ne pas correspondre au type de langage emplyé. Pour ce qui est de l'infographie par exemple, on utilise généralement des langages impératifs avec une modélisation objet. Et la manière de programmé ressemblera à de l'objet, mais dans un langage impératif.
Il ne faut pas oublier quà la fiin, on a de l'assembleur, qui est un langage impératif de très bas niveau. Mais la structure du code pourra être modélisé en objet

Oui, on peut faire de l'objet sans langage objet, merci, je sais

Un langage objet c'est juste des facilités en plus proposées des mécanismes supprémentaires

Mais sérieux c'est vraiment que dans des cas pointu qu'on fait tout en assembleur... Ça touche quel pourcentage des programmeurs ? Les systèmes critiques, c'est quelle proportion ? Presque rien.

La grande majorité utilise des langage de haut niveau parce que programmer en asembleur c'est bien beau mais c'est énormément plus coûteux, chiant, etc... De même, les peuves de programme, c'est joli sur le papier mais ça va pour la petite portion super critique du programme (quand le programme en contient une, ce qui est rare), c'est tout...

La majorité des développeurs n'utiliseront jamais un prouveur dans leur vie professionnelle, pas plus qu'ils ne programmeront en assembleur...
_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 13:06

C'est pas parce que la plus part le font que c'est bien... D'ailleurs, la majorité des programmes trouvables dans le commerce possèdent au moins un bug

Par contre, les applications critiques touchent bien plus de secteru que tu le penses, tout ce qui touche à la sécurité. Pour l'aérontique, ils ont en fait un langage de moyen niveau spécifique prouvanle dont le compilateur est fait en assembleur quand ça n'est pas fait directement dans ce langage. Faut pas avoir une Windows Fatal Error, veuillez rebboter la machine en plein vol

Citation :

C'est pas parce qu'on permet des trucs pas propre dans le langage en général qu'on ne peut pas prouver un programme... De base je vois pas où c'est contradictoire...

Là, tu me déçois.. SI on peut faire des trucs sales, on peut pas prouver des trucs car on peut dériver une fonction du programme afin de lui faire faire autre chose. Par exemple, en Ada, si un programme contient juste une boucle For, tu sais qu'il se terminera (par une erreur ou pas, avec le résultat escompté ou non), mais il se terminera. En C, c'est impossible car tu peux modifier l'itérateur de la boucle afin de simuler un while.

Code :

for(i=1;i<10;i++)
{
i--;
}

Par exemple...
Cela empêche la création de règles efficaces pour ce langage, ce qui au final empêche dans la majorité des cas de faire une preuve du programe. L'intérêt des preuves, c'est que TOUT programme du langage peut être prouvé, pas uniquement ceux codé d'une certaine manière.
Ajoute à ça les effets de bord, une mauvaise gestion des variables locales et des types...

| Profil | MP | Site web

Dernière édition par Lumen le 01 Oct 2005 13:38; édité 1 fois

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 13:13

L'intérêt de prouver un programme c'est de prouver que lui va marcher... On s'en tape de savoir si tout programme écrit dans ce langage sera prouvable, du moment qu'on peu prouver celui qui nous intéresse :eh:

_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web

Lumen

Illusioniste

Inscrit le : 03 Sep 2005
Messages : 878
Séries favorites : Flander's Compagny, le Visiteur du Futur

Posté le : 01 Oct 2005 13:17

Darathor a écrit :

L'intérêt de prouver un programme c'est de prouver que lui va marcher... On s'en tape de savoir si tout programme écrit dans ce langage sera prouvable, du moment qu'on peu prouver celui qui nous intéresse

Ca va dépendre de pas mal de chose... Si on peut extraire une sous grammaire de la grammaire du langage qui est prouvable, on en revient en fait à avoir un langage entièrement prouvable
Par contre, si une telle sous-grammaire n'est pas trouvé, je doute qu'on puisse alors prouver quelque chose, et même si c'est le cas, on aura un programme difficile à remanier car chaque modification, même légère, forcera à refaire entièrement une preuve.

| Profil | MP | Site web

Darathor

Mage-Administrateur
Archangemage

Inscrit le : 28 Oct 2001
Messages : 27741
Points : 21 Concours jeux - 30e place

170

Localisation : Strasbourg
Séries favorites : Last Exile, Gunslinger Girl, Noir, Monster, Buffy/Angel, Stargate, Battlestar Galactica, Rome, Monster...

Posté le : 01 Oct 2005 13:23

J'ai pas dit que c'était le paradis non plus et qu'il suffisait de claquer des doigts, sinon on ne travaillerait qu'avec des programmes prouvés et sans bugs :-D

Toujours est-il que le CAML reste un truc exotique, sûrement utilisable en théorie et même utilisé dans quelques rares cas, mais que la majorité des étudiants ne rencontreront probablement plus jamais une fois sortis de la fac...

PS : Je sais pas s'il y a des langages où ton exemple de for est syntaxiquement correct mais le C n'en fait certes pas partie

_________________

Je fais appel à la puissance des éthers | Soyez le bras armé de ma colère | Que le Cataclysme se déchaine !

| Profil | MP | E-mail | Site web