Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
[Anubis2] Longueur des programmes
Une question au créateur d'Anubis2 :
Sachant qu'un solveur de Sudoku s'écrit en une vingtaine de lignes en OCaml, et en un peu plus de 5000 lignes (en comptant néamoins les commentaires) en Coq, le tout accompagné d'une notice de 13 pages en PDF, où se situera l'équivalent en Anubis2 et quelles seront les assurances données ? Juste que ça termine, ou bien que ça retourne toujours la bonne solution si elle existe ?
Merci
C'est sans doute dû au problème posé (Sudoku) plus qu'à la structure de COQ. Par ailleurs, je ne sais pas ce que cette preuve prouve précisément. Sans doute pas seulement la terminaison.Envoyé par alex_pi
Bien entendu, écrire un algorithme est une chose, prouver qu'il a telle ou telle propriété en est une autre, et il n'y a aucune correlation a priori entre les tailles des deux textes. Un exemple très simple est le problème de Syracuse: On a la fonction f suivante, définie sur les entiers et à valeurs dans les entiers
Ces trois lignes forment un programe de calcul très simple. La question est qu'il n'y a aucune garantie qu'il termine. Prouver qu'il termine (ça sera forcément sur la valeur 1 d'ailleurs tel qu'il est écrit ici) est encore une conjecture aujourd'hui. Si un jour on en trouve une preuve, il est probable qu'elle sera monstrueuse.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3
4
Le programme ci-dessus peut être écrit en Caml et en Anubis 1, mais pas en Anubis 2, tant qu'on ne saura pas démontrer que ça termine. En effet, le compilateur Anubis 2 oblige le programmeur à passer sous les fourches caudines des schémas de récursion. C'est l'un des éléments qui assurent que tous les programmes Anubis 2 purs terminent. je ne parle bien sûr que des programmes purs (aucune manipulation d'objet concrêt).
Je pourrais d'ailleurs prendre un autre exemple pour montrer la différence de philosophie. Imaginons qu'on veuille écrire un programme pour réduire les termes du lambda-calcul typé. C'est très simple d'itérer la beta-réduction, et on peut faire un programme Caml très court faisant cela. Par contre, un programme en Anubis 2 pur faisant la même chose contient nécessairement une preuve du théorème de Tait. Il est donc certainement beaucoup plus long, et évidemment très loin d'être trivial. Je suppose qu'il en serait de même en COQ.
Pour ce qui est du Sudoku, tout dépend de ce qui est prouvé. S'il s'agit à la fois de la terminaison, de l'unicité ou du caractère optimal de la solution, que sais-je encore, ça peut être long effectivement. Pour ce qui est des assurance données et de la taile de la preuve, cela devrait être comparable à ce qu'on fait en COQ. C'est plus la nature du problème qui compte que le langage.
Ce qui est surtout important dans l'industrie est le fait que le programme fasse ce qu'on veut qu'il fasse. Le meilleur moyen de s'en assurer reste quand même de se donner des moyens formels de preuve. C'est ce qui a été fait pour le logiciel de la ligne 14 du métro, fait en système B. Le source est certainement plus long que ce qu'il aurait été sans les preuves, mais on a sans doute jugé que l'investissement était rentable. On n'a jamais constaté de bug sur ce programme. On a donc évité les frais de mise au point, les ennuis et le stress. De toute façon la sécurité a un prix, et plus ça va plus on exige de sécurité, et plus on est prêt à payer pour cela. Je pense donc que l'avenir est aux langages à preuves, même si cela doit changer la façon de tavailler des développeurs.
Pour en revenir quand même à Anubis 2, je fait tout pour qu'il soit très proche des maths usuelles. C'est bien sûr un des aspects importants sur lequels je mise.
Non, probablement pas ! Je pense que ça prouve que s'il existe une solution, il la trouve, que s'il en existe plusieurs, il les trouve toutes, etc. (en plus de la terminaison, qui est une nécessité en Coq)
L'indécidabilité nous enquiquinera toujours...
Je vous ai envoyé mon cursus actuel par MP, vous vous doutez bien que je ne vais pas faire une opposition frontale ! Mais je ne suis néamoins pas entièrement d'accord. Il y a des domaines où l'ont veut avoir des assurances que ça se passe bien. Quand on conduit un Métro, on fait appelle au système B et à ses boites, quand on pilote un A380, on fait vérifier son code par Astrée, et je suis bien content qu'un compilateur C certifié soit en bonne voie. En revanche, je pense que le cas du sudoku est parlant. Quand on voit que l'on multiplie le nombre de ligne par plus de 100, et que la seconde version nécessite probablement un niveau bac+4 pour être comprise, et bac+5 pour être écrite, on se dit que non, ce n'est pas "l'Avenir", avec un grand 'A'. On n'est pas pret de prouver que le noyau de mon OS ou même mon client mail font exactement ce que l'ont veut, et tant pis (et d'ailleurs, heureusement qu'on ne prouve pas qu'ils terminent, ça m'ennuierai :-))
Et c'est la raison de ma question sur Anubis2. Si c'est un système de preuve complet, en quoi sera-t-il plus utilisable par un humain normal que Coq (qui est, admettons le, plutot ardu à appréhender), ou qu'apportera-t-il par rapport à ce qui existe déjà. Si ce n'est pas le cas, qu'aportera-t-il de plus qu'un typage statique fort "à la ML", et surtout, à quel prix ? Pour écrire un solveur de sudoku dont on prouvera simplement qu'il termine, sans forcément prouver quoi que ce soit sur la solution, à combien entre 20 et 5000 lignes de code évaluez vous la chose ? Bref, peut-on en savoir un peu plus que "il s'appuie sur les mathématiques" ce qui veut tout dire et rien à la fois ?
Il est tard et je ne pourrai pas répondre sans doute avant mercredi (j'enseigne les lundis et mardi). En attendant, je te recommande ce document qui est assez instructif:
http://www.univ-valenciennes.fr/ROI/...rian-Petit.pdf
Très certainement Astrée a du jouer un rôle important pour l'A380, mais leur techniques de génération de code et de programmes sont beaucoup plus poussées que ce que l'on pourrait croire. Entre autres, l'utilisation de Lustre facilite grandement la tâche. On n'écrit quasiment pas de code C embarqué chez Airbus : les seules parties écrites en dûr, en C, sont celles concernant les entrées-sorties, que l'on ne peut faire en Lustre. Tout le reste, c'est du Lustre.
Ca c'est ce qui concerne l'avionique... bien-sûr, le serveur de films embarqué n'est pas fait comme ceci... si il tombe en panne, c'est pas trop grave... tout au plus on s'ennuira un peu pendant le voyage !
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Je ne sais pas, mais au final, il y avait quand même plus de 500 000 lignes de code C à vérifier ! C'est un peu long à la main :-) Après, ce code C est peut-être une compilation de Lustre, je n'en sais rien.
Je suis tout comme toi dans le questionnement, tout comme toi je me hasarde à faire des suppositions, ici j'en fais deux:
- Si un jour je peux lire une source COQ ce sera grâce à DrTopos qui m'a considérablement déblayé le terrain, COQ pourrait me paraître beaucoup plus accessible qu'il me paraîssait il y a peu. En tout cas je n'ai pas connaissance d'un tutoriel sur le sujet qui soit plus accessible que le quizz de DrTopos.
- Je ne crois pas que la longueur de la preuve soit un critère, et ce quelle que soit la façon dont on la mesure.
Par contre je m'intéresse à la qualité de la preuve:
- Est-elle facultative ou obligatoire ? Intuitivement je dirais facultative parce que le type de (x:One) |-f-> f x est One -> $T et celà me paraît un type valide. Si j'ai raison celà répondrait un peu à ta question: contrairement à COQ et Epigram le langage des termes serait Turing-complet. Dans tous les cas le langage des énoncés n'est pas Turing-complet. COQ et Epigram t'obligent à travailler avec le langage des énoncés. Avec Anubis 2 tu écrirais des termes que tu pourrais ensuite décorer avec des énoncés.
- Est-elle incrémentale ? Par exemple je viens de programmer un AVL. Si la preuve est facultative je peux ne rien prouver du tout. Puis dans un élan salvateur je peux vouloir prouver que je construis et maintiens bien un ABR, juste en ajoutant des énoncés, sans toucher à l'implémentation. Enfin je serais bête de pas prouver que mon ABR est équilibré, toujours en ajoutant des énoncés, sans toucher à l'implémentation. Tu ne peux pas le faire en COQ ou Epigram parce que tu ne peux pas créer une expression sans écrire exhaustivement son énoncé.
Par rapport à ML/Haskell, Anubis 2 ajoute une nouvelle couche de typage (facultatif). COQ ou Epigram jettent tout le système auquel tu es habitué, tu ne peux plus écrire let rec f () = f ();; car c'est tout simplement mal typé.
Honnêtement, je ne connais pas actuellement d'autre proposition capable d'augmenter le typage à la ML comme je crois qu'Anubis 2 pourrait le faire.
EDIT
Celà va sans dire toutefois c'est mieux en le disant:
Si on écrit (x:One) |-f-> f x on ne pourra écrire aucun énoncé bien typé qui affirmerait une propriété de f. Pourquoi? Parce qu'une fonction récursive est l'implémentation d'un raisonnement par récurrence. Le raisonnement inductif doit rester acyclique.
- Ne pas pouvoir prouver n'interdira pas d'écrire
- Le fait d'écrire ne garantira pas que l'on puisse prouver sans modifier le code
- Si on a l'intention de prouver un énoncé alors il existe une façon raisonnable de l'implémenter sans modifier le code
- D'une façon générale il n'existe pas de façon raisonnable de prouver des énoncés raisonnables
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Il y a une chose qu'il faut bien comprendre à propos de la terminaison des programmes. Quand je dis qu'en Anubis 2 tous les programmes terminent, je ne parle que des programmes purs, c'est à dire ne faisant intervenir aucun objet concrêt (comme fichier, connexion, fenêtre graphique, etc....). Il est bien certain qu'un serveur web est dans une boucle d'écoute infinie, et que c'est bien ce qu'on désire. Mais un serveur écoute sur une connexion, qui n'est pas un objet abstrait, mais un objet concrêt, et ne peut donc pas être un programme pur,
Je suppose qu'il doit en être de même en Coq. D'ailleurs, peut-on faire un serveur en Coq, ou bien Coq se limite-t-il aux programmes purs ?
Un programme pur, c'est à dire un programme sans aucun lien avec l'extérieur (pas d'effet de bord, pas de lecture de connexion,...) n'a aucune raison de ne pas terminer. S'il ne termine pas, je pense qu'on peut considérer qu'il est planté, puisque de toute façon sa seule raison d'être est de renvoyer une valeur. Pour cela, il faut bien qu'il s'arrête.
Lancer l'execution d'une fonction récursive pure partielle, dont on n'est pas sûr qu'elle s'arrête, ne me semble pas raisonnable, à moins de garder le doigt sur [Ctrl-C].
Donc en ce qui concerne la programmation pure, je ne pense pas que Turing-complet soit un critère intéressant, et je crois que certains profs d'informatique en rajoutent un peu. N'importe quel programme faisant quelquechose d'utile peut très probablement être programmé avec seulement des fonctions dont on sait (pour une raison générale établie une fois pour toutes, par exemple) qu'elles terminent toutes.
En conséquence, si tu programme un OS en Anubis 2 (dans l'état actuel des choses, je ne peux pas dire si ce serait une bonne idée ou non), le compilateur ne te demandera pas de prouver la terminaison, puisqu'un OS est (presque par définition) un programme manipulant des objets concrêts.
Aucun système (cohérent) de preuve n'est complet. Cela résulte du théorème d'incomplétude de Gödel. On trouvera toujours des énoncés indécidables, c'est à dire qu'il sera toujours possible de rajouter de nouveaux outils de preuve. L'essentiel est d'en avoir assez pour pouvoir faire toutes les maths usuelles.
Pour ce qui est d'Anubis 2, je pense qu'il y aura deux différences avec l'existant.
- Je fais le maximum pour que mon langage ressemble aux maths usuelles, c'est à dire que quiconque est un peu habitué à faire des maths devrait pouvoir faire de l'Anubis 2 presque sans apprentissage. Je me demande même s'il y aura un langage s'écrivant linéairement (dans un fichier texte). Je tends de plus en plus vers un logiciel interactif graphique (une sorte d'éditeur-compilateur intégré), justement pour en faciliter l'usage.
- La sémantique n'est pas la même que celle des langages basés sur la théorie de Martin-Löf (comme c'est le cas de Coq). La théorie de Martin-Löf est exotique en ce sens qu'il existe des inclusions canonique de sous-types dans des types dont l'injectivité est indécidable, voire fausse. Aucun mathématicien ne fera des maths avec une telle théorie, alors que la sémantique dans les topos me garantie que la sémantique d'Anubis 2 est conforme aux mathématiques usuelles. Cela concerne Coq, Nuprl et quelques autres, mais peut-être pas PVS, ... Je ne les ai pas examinés de tellement près.
Je pense qu'on pourra se rendre compte de ce dernier point (la ressemblance avec les maths usuelles) si on va assez loin dans le quizz.
A propos de Coq, il y a une chose qui me travaille, et j'aimerai bien qu'il y ait quelqu'un connaisant assez bien Coq (et pouvant expérimenter avec) pour me répondre. Le principe de 'proof-irrelevance' est incompatible avec la théorie de Martin-Löf (c'est à dire que Martin-Löf + proof-irrelevance est contradictoire), or l'axiome 'proof-irrelevance' a été introduit en Coq. Comment on-t-ils fait pour éviter l'effondrement du système (s'ils l'ont fait) ?
Ca m'a tout l'air d'être incorrect ce que tu dis-là : si c'était le cas, alors tous les programmes Haskell devraient terminer par essence même... or ce n'est pas le cas, et le langage reste on ne peut plus pur. Si une valeur prend un temps indéfiniment long pour être calculée, il y a des chances pour que ton programme ne se termine pas, et pourtant il reste pur !
Encore une fois, il me semble que vouloir trop théoriser et mélanger délires de mathématiciens avec informatique est une très mauvise idée... c'est mon avis, ça n'engage que moi.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Je ne suis pas d'accord. Haskell n'est pas pur au sens ou je l'entends. La monad IO ne fait pas partie du pur, puisqu'il y a une connexion ou un fichier derrrière. Tu joues sur les mots là.
Et puis, je ne délire pas ... mais alors pas du tout....
Steki-kun est certainement le mieux placé pour répondre à cette question, mais je fais essayer de dire ce que j'en pense avec les quelques séances de Coq que j'ai faites
1) Coq fait très peu de preuves seul, il faut expliquer chaque étape à l'aide de règles logique... il existe des "stratégies", mais elles ne m'ont jamais semblé très puissantes (je précise que je n'ai pas tout testé)
2) on peut ajouter un axiome dans Coq, et de toute façon, ça permet d'avancer pour prouver les étapes intermédiaires du calcul en cours, mais c'est à l'utilisateur de dire quand l'appliquer... aucune stratégie automatique ne le fera
Nan, c'est pas ça qu'il veut dire (du moins ce n'est pas comme ça que je le comprends)
Evidement, en lambda calcul, qui me semble franchement "pur" dans le "sens" que j'en perçois, on peut écrire des fonctions qui ne terminent pas. Sinon le théorem qui dit que le problème de l'arret est indécidable aurait tout l'air d'etre faux :-)
Ce qu'il faut voir, c'est qu'un programme "pur" qui ne termine pas n'a aucun intéret. Il ne fait pas d'entrée sortie (puisqu'il est pur), et il ne retourne pas de valeur, puisqu'il ne termine pas. Bref, il ne sert à rien. Donc se limiter aux programmes qui terminent (comme le fait Coq) n'est pas forcément une grosse limitation. Après, le hic, c'est que pour faire cette limitation, soit il faut réduire de façons drastique le langage, pour que le compilo se débrouille avec les preuves, soit il faut donner à l'utilisateur la possibilité de prouver à la main. Et après, il faut trouver des utilisateurs pret à le faire, et c'est pas gagné :-)
C'est pas gagné... à moins que la preuve soit facultative.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Il est impossible en Coq d'écrire une fonction qui ne termine pas.
Faites gaffe de ne pas trop virer Jayce (créateur de feu MultiDeskOS) quand même hein...
Je ne voulais pas dire complet au sens mathématique de la complétude, mais au sens de "un peu plus avancé qu'un système de type" par exemple (puisqu'un typage d'un programme ML est une preuve d'un certain nombre de choses). Bref, je ne donnais pas de sens formel à "complet"
Euh... je ne suis pas sûr de voir le lien entre la partie droite et la partie gauche du "c'est à dire" là.
Et d'où tenez vous qu'aucun mathématicien ne travaillerai avec une telle théorie ? Il me semble, par exemple, que l'ensemble des maths jusqu'à la license a été reformalisé en Coq. Et que des matheux en Géométrie algébrique (je ne suis plus sûr du domaine) reprouve leurs théorèmes en Coq, parce qu'ils en arrive à avoir des doutes sur l'ensemble strict d'hypothèse qu'ils utilisent pour leur théorèmes vu le niveau d'abstraction.
Pour la quesiton sur Coq, je ne sais pas. En revanche, si j'ai bien regardé, il n'a pas été "introduit dans Coq", mais est effectivement chargeable. Pour ce qui est de l'incohérence, je ne trouve rien là dessus sur google. Je creuserai, un jour.
Il n'est pas facile de trouver des théorèmes d'arithmétique qui ne se prouve pas d'un bon coup de "omega" apparement
Les théorèmes à prouver seraient bien tristes sans axiomes :-)2) on peut ajouter un axiome dans Coq, et de toute façon, ça permet d'avancer pour prouver les étapes intermédiaires du calcul en cours, mais c'est à l'utilisateur de dire quand l'appliquer... aucune stratégie automatique ne le fera
Pour ce qui est des tactics, pour auto et ses variantes, on peut leur dire d'utiliser des axiomes ou des lemmes. Et on peut écrire ses propres tactics, utilisant ses axiomes et ses lemmes.
Pareil en Epigram, on ne peut pas programmer une fonction dont une application pourrait ne pas terminer.
COQ je ne connais que de réputation.
En clair:
One est un type concrêt.
Donc en Anubis 2 je pourrai écrire (x:One) |-f-> f(x).
Cette fonction sera de type One -> $T.
Son application sera autorisé (et ne terminera pas).
C'est bien ce que tu désire alex_pi, non ?
Bien sûr on ne pourra pas écrire un énoncé ?x:One E où E contient l'expression f(x). Mais on s'en fiche puisque cet énoncé ne sert à rien.
L'astuce: si le système de preuve t'embête, tu ajoute un argument de type One et il te fiche la paix.
Manifestement de alex_pi ou moi il y en a au moins un qui n'accroche pas les wagons à la locomotive.
Alors si je suis le maillon faible, pitié dites-le moi.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Cela va un peu vite ce soir sur ce fil. Il faut quand même que je trouve le temps de répondre à SpiceGuid.
En Anubis 2, on ne pourra pas écrire (x:One) |-f-> f(x), tout simplement parce que le type One n'est pas récursif. Les fonctions récursives ne se définissent qu'avec un type récursif à la source (ou un produit de types dont un au moins est récursif).
Pour ce qui est du caractère facultatif des preuves, non les preuves ne seront pas facultatives, ou du moins s'il en manque une, le compilateur mettra un warning pour bien signaler qu'il décline toute responsabilité. Cela peut être un outil utile pendant le développement, évidemment, mais dans un produit fini tout ce qui est affirmé doit être prouvé. (En système B, on parle d'obligation de preuve)
One n'est pas un type concrêt. C'est un type abstrait (au sens où je l'entends). Les données de type One n'ont pas d'état interne variant au cours du temps. Par contre un type de connexion réseau est un type concrêt, puisque les connexions ont un état interne qui varie dans le temps. Les mathématiques ne se font qu'avec des types abstraits. C'est d'ailleurs, ce qui rend d'une certaine façon l'informatique plus difficile que les maths: il faut aussi manipuler les données des types concrêts. D'ailleurs, on devrait faire une distinction plus nette que cela. Je propose de parler de type et de donnée pour ce qui est abstrait, et de classe et d'objet pour ce qui est concrêt. Par exemple, un nombre est une donnée, mais une connexion est un objet.
Le critère fondamental est qu'une donnée est indépendante du temps, alors qu'un objet dépend du temps (il est créé ou ouvert à une certaine date, il est fermé ou détruit à une autre, son état interne change avec le temps, de plus il n'est pas marshalisable). Une donné abstraite ne dépend pas du temps. Elle a un sens invariable dans le temps et ne peut être ni créée ni détruite (c'est le cas de tous les objets mathématiques, qui ne sont donc pas des objets au sens ci-dessus !). Par ailleurs, les données abstraites ne sont pas soumises au principe d'identité de la POO. C'est aussi une façon de les distinguer des objets.
Puisqu'on est dans les définitions, voici ce que j'entends par terme déterministe: un terme qui n'a à voir qu'avec des choses abstraites. C'est important pour un compilateur dans la phase d'optimisation. Par exemple, mettre en facteur deux exemplaires d'un même terme n'est sûr que s'il est déterministe. En C, un terme déterministe est l'équivalent d'une constante (une chose calculable une fois pour toutes à la compilation).
Bien sûr, tout cela impose un ensemble de contraintes très strictes, mais c'est nécessaire pour ne pas rendre inutile le système de preuve en l'effondrant logiquement. La solution est de mettre des surcouches ``intelligentes'', comme par exemple un programme de recherche de preuve, pour éviter d'avoir à tout écrire, ou bien de concevoir une couche de langage plus naturelle qui est traduite en choses plus formelles par le compilateur. Toutes ces choses là ne font plus partie de la logique. On touche plutôt à l'intelligence artificielle ou à l'ergonomie.
En fait on pourra procéder en Anubis 2 par raffinement. C'est à dire qu'on peut programmer quelque chose, qui sera donc nécessairement formellement correct, mais qu'on peut par la suite vouloir affiner par des restrictions supplémentaires. Il suffit alors de changer certains énoncés pour changer les contraintes. Evidemment, le compilateur va être amené à réclamer de nouvelles preuves.
Haskell est le plus pur des langages de programmation que je connaisse : les monades ont été inventées pour justement ne pas casser le caractère pur, et c'est entre autres pour celà que l'on ne peut JAMAIS sortir une valeur hors d'une monade. Les monades sont des valeurs comme les autres : certaines prennent un temps infini pour être évaluées, d'autres non. Je soutiens que ce n'est pas jouer sur les mots. Je pense qu'il y a un vrai problème ces derniers temps à tout vouloir prouver, démontrer, axiomatiser, formaliser, surtout lorsque ça n'ajoute rien au sens et au débat : il faut sortir la tête du bocal un peu, prendre l'air ! La programmation, ça reste de la programmation.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Ce genre de message d'opinion me paraît hors sujet, si on ne peut pas parler de preuve sur le forum fonctionnel alors qu'on me dise sur quel forum on peut en parler.
Si tu refuse d'identifier la récursivité avec la récurrence alors Haskell fait très bien l'affaire, qui a dit que Haskell ne fait pas ton affaire ? Celà a toujours été un principe de la programmation fonctionnelle de rapprocher récursivité et récurrence. Le projet est noble en soi. Pourquoi tenter d'isoler un intelocuteur de qualité ? Pour le convertir ? Vous savez bien que ça n'est pas possible. Et cette insistance à vouloir que votre interlocuteur utilise votre vocabulaire au lieu de chercher à comprendre le sien, au premier contact c'est compréhensible mais à force de répétition celà montre un certain déficit de curiosité.
@InOcamlWeTrust
Parlerais-tu de la même façon à un programmeur COQ ?
EDIT: Quand on parle de preuves formels on parle de pionniers, tu ne peux pas ignorer qu'à la traîne il y a toute une industrie des services informatique qui est obsédée par la productivité et qui n'intègre les gains en qualité que par la peur d'être larguée. Moins il y a de distance entre eux et la tête plus ils n'améliorent que la productivité.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Prouver certaines choses, oui, comme des programmes CRITIQUES, mais prouver n'importe quoi, non.
Ce que je déplore, c'est que certaines personnes n'aient pas conscience que l'informatique est une science et un domaine à part entière.
De plus, tu dis que l'industrie est très friande de ce genre de choses... peut-être, et encore, il faudrait savoir de quelle industrie on parle-là ! Celle que je connais, la simulation numérique, s'en moque éperdûment, car les gens qui travaillent dans ce type de projets n'ont pas besoin que chaque ligne de code soit passée au crible : ce qui compte, c'est la robustesse, d'avoir des résultats justes (tout en calculant faux) et d'être extrêmement performant.
Dans un autre domaine : Airbus et Schneider Electric y accordent beaucoup d'importance, entre autres, du fait que ce sont des automaticiens qui écrivent le code critique, et non des informaticiens ; Boeing beaucoup moins. Pourtant, les avions de Boeing volent !
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Répondre avec citation
Partager