J'ai remarqué qu'il m'est beaucoup plus facile d'écrire des preuves mathématiques sans commettre d'erreur, que d'écrire un programme d'ordinateur sans bugs.

Il semble que ce soit quelque chose de plus répandu que mon expérience. La plupart des gens font constamment des bogues logiciels dans leur programmation et ils ont le compilateur pour leur dire quelle est l'erreur tout le temps. Je n'ai jamais entendu parler de quelqu'un qui a écrit un gros programme informatique sans commettre d'erreur, et qui était confiant que ce serait sans faille. (En fait, presque aucun programme n'est sans utilisation, même beaucoup de ceux très débogués).

Cependant, les gens peuvent écrire des articles entiers ou des cahiers d'épreuves mathématiques sans qu'aucun compilateur ne leur dise jamais qu'ils ont commis une erreur, et parfois même sans avoir l'avis d'autres personnes.

Laisse moi être clair. Cela ne veut pas dire que les gens ne font pas d'erreur dans les preuves mathématiques, mais pour les mathématiciens même les plus expérimentés, les erreurs ne sont généralement pas aussi problématiques et peuvent être résolues sans l'aide d'un "oracle externe", comme un compilateur pointant vers votre erreur.

En fait, si ce n'était pas le cas, les mathématiques seraient difficilement possibles, me semble-t-il.

Cela m'a donc amené à poser la question suivante: Qu'est-ce qui est si différent à écrire des preuves mathématiques irréprochables et à écrire du code informatique irréprochable qui fait en sorte que le premier est tellement plus souple que le second?

On pourrait dire que c'est simplement le fait que les utilisateurs disposent de "l'oracle externe" du compilateur pour signaler leurs erreurs qui rend les programmeurs paresseux, les empêchant de faire le nécessaire pour écrire du code de manière rigoureuse. Cela signifierait que s’ils n’avaient pas de compilateur, ils pourraient être aussi irréprochables que des mathématiciens.

Cela peut sembler persuasif, mais si je me base sur mon expérience de la programmation et de la rédaction de preuves mathématiques, il me semble intuitivement que ce n’est vraiment pas une explication. Il semble y avoir quelque chose de plus fondamentalement différent dans les deux entreprises.

Ma pensée initiale est que, quelle que soit la différence, c’est que pour un mathématicien, une preuve correcte ne nécessite que chaque étape logique. Si chaque étape est correcte, la preuve entière est correcte. D'autre part, pour qu'un programme soit sans image, non seulement chaque ligne de code doit être correcte, mais sa relation avec toutes les autres lignes de code du programme doit également fonctionner.

En d'autres termes, si l'étape d'une preuve est correcte, une erreur à l'étape ne gâchera jamais l' étapeMais si une ligne de code est correctement écrite, alors une erreur dans la ligne aura une influence sur le fonctionnement de la ligne , de sorte que chaque fois que nous écrivons la ligne nous devons tenir compte de sa relation avec toutes les autres lignes. Nous pouvons utiliser l'encapsulation et toutes ces choses pour limiter cela, mais cela ne peut pas être supprimé complètement.Y X X Y X $X$$Y$$X$$X$$Y$$X$$X$

Cela signifie que la procédure de vérification des erreurs dans une preuve mathématique est essentiellement linéaire dans le nombre d'étapes de vérification, mais que la procédure de vérification des erreurs dans le code de calcul est essentiellement exponentielle dans le nombre de lignes de code.

Qu'est-ce que tu penses?

Remarque: Cette question comporte un grand nombre de réponses qui explorent une grande variété de faits et de points de vue. Avant de répondre, veuillez les lire tous et ne répondez que si vous avez quelque chose de nouveau à ajouter. Les réponses redondantes ou les réponses qui ne sauvegardent pas les opinions avec des faits peuvent être supprimées.

Permettez-moi d’offrir une raison et une idée fausse pour répondre à votre question.

La principale raison pour laquelle il est plus facile d'écrire (en apparence) des preuves mathématiques correctes est qu'elles sont écrites à un très haut niveau. Supposons que vous puissiez écrire un programme comme celui-ci:

function MaximumWindow(A, n, w):
    using a sliding window, calculate (in O(n)) the sums of all length-w windows
    return the maximum sum (be smart and use only O(1) memory)

Il serait beaucoup plus difficile de se tromper en programmant de cette façon, car la spécification du programme est beaucoup plus succincte que sa mise en œuvre . En effet, chaque programmeur qui tente de convertir un pseudo-code en code, notamment en code efficace, rencontre ce gouffre entre l’ idée d’un algorithme et les détails de son implémentation . Les preuves mathématiques se concentrent davantage sur les idées et moins sur les détails.

La contrepartie réelle du code pour les preuves mathématiques est la preuve assistée par ordinateur . Celles-ci sont beaucoup plus difficiles à développer que les preuves textuelles habituelles, et on découvre souvent divers recoins cachés qui sont "évidents" pour le lecteur (qui ne les remarque généralement même pas), mais pas si évidents pour l'ordinateur. De plus, étant donné que l'ordinateur ne peut actuellement combler que des lacunes relativement minimes, les preuves doivent être élaborées à un niveau tel qu'un homme qui les lira manquera la forêt pour les arbres.

Une idée fausse importante est que les preuves mathématiques sont souvent correctes. En fait, c'est probablement plutôt optimiste. Il est très difficile d’écrire des preuves compliquées sans erreur et les papiers contiennent souvent des erreurs. Peut-être les plus célèbres cas récents sont la première tentative de Wiles à (un cas particulier de) le théorème de modularité ( ce qui implique le dernier théorème de Fermat), et diverses lacunes dans la classification des groupes simples finis, y compris certains 1000+ pages groupes quasithin qui étaient écrit 20 ans après la fin supposée du classement.

Une erreur dans un article de Voevodsky lui a tellement fait douter des preuves écrites qu'il a commencé à développer la théorie des types d'homotopie , un cadre logique utile pour développer formellement la théorie de l'homotopie, et a dorénavant utilisé un ordinateur pour vérifier tous ses travaux ultérieurs (du moins selon sa propre théorie). admission). Bien qu’il s’agisse d’une position extrême (et pour le moment peu pratique), il reste que lorsqu’on utilise un résultat, il convient de passer en revue la preuve et de vérifier si elle est correcte. Dans ma région, il existe quelques papiers qui sont connus pour être faux mais qui n'ont jamais été rétractés, et dont le statut est relayé de bouche à oreille parmi les experts.

(Je risque probablement quelques critiques négatives ici, car je n’ai ni le temps ni l’intérêt d’en faire une réponse appropriée, mais je trouve que le texte cité (et le reste de l’article cité) ci-dessous est assez perspicace, compte tenu également de leur rédaction. par un mathématicien bien connu, je pourrais peut-être améliorer la réponse plus tard.)

L'idée, qui, je suppose, n'est pas particulièrement distincte de la réponse existante, est qu'une "preuve" ou un argument communique avec une communauté mathématique, dans le but de la convaincre que les détails (fastidieux) peuvent être renseignés, en principe, pour obtenir une preuve formelle entièrement spécifiée - sans souvent le faire du tout. Un exemple critique de ceci est que vous pouvez utiliser des théorèmes existants en les énonçant simplement, mais la réutilisation de code est beaucoup plus difficile en général. Pensez également aux "bogues" mineurs, qui peuvent complètement rendre un morceau de code inutile (par exemple, il s'agit de SEGFAULT), mais peuvent laisser un argument mathématique en grande partie intact (c'est-à-dire, si l'erreur peut être contenue sans que l'argument ne soit réduit).

La norme d'exactitude et d'intégralité nécessaire pour faire fonctionner un programme informatique est supérieure de quelques ordres de grandeur à la norme de preuve valide de la communauté mathématique. Néanmoins, les gros programmes informatiques, même lorsqu'ils ont été écrits et testés avec soin, semblent toujours avoir des bogues. [...] Les mathématiques telles que nous les pratiquons sont beaucoup plus formellement complètes et précises que les autres sciences, mais elles sont beaucoup moins formellement complètes et précises pour ce qui est du contenu que les programmes d'ordinateur. La différence ne tient pas seulement à la quantité d'effort: le type d'effort est qualitativement différent. Dans les grands programmes informatiques, il faut consacrer une énorme partie de l’effort à la myriade de problèmes de compatibilité: s’assurer que toutes les définitions sont cohérentes, en développant de "bonnes" structures de données qui ont une généralité utile mais non encombrante, décidant de la "bonne" généralité pour les fonctions, etc. La proportion d'énergie dépensée pour la partie active d'un programme volumineux, à la différence de la partie comptabilité, est étonnamment petite. En raison de problèmes de compatibilité qui dégénèrent presque inévitablement du fait que les "bonnes" définitions changent à mesure que la généralité et la fonctionnalité sont ajoutées, les programmes informatiques doivent généralement être réécrits fréquemment, souvent à partir de zéro.

SUR LA PREUVE ET LES PROGRÈS EN MATHÉMATIQUES (pp. 9-10), par WILLIAM P. THURSTON https://arxiv.org/pdf/math/9404236.pdf

Permettez-moi de commencer par citer EW Dijkstra:

"La programmation est l'une des branches les plus difficiles des mathématiques appliquées; les mathématiciens les plus pauvres auraient intérêt à rester de purs mathématiciens." (à partir de EWD498)

Bien que ce que Dijkstra voulait dire par `programmation 'diffère un peu de l’usage actuel, cette citation a encore un certain mérite. Les autres réponses ont déjà indiqué que le niveau d'abstraction en mathématiques pouvait être beaucoup plus élevé qu'en programmation, ce qui signifie que nous pouvons ignorer certains aspects délicats si nous le souhaitons.

Cependant, j'estime qu'il s'agit simplement d'une conséquence d'une différence plus fondamentale entre une preuve et un programme informatique, qui est leur objectif .

Le but principal d'une preuve mathématique est, entre autres, de se convaincre qu'une revendication mathématique est correcte et, peut-être encore plus important, de parvenir à la compréhension . Par conséquent, vous pouvez choisir de ne travailler que dans le monde mathématique, où tout est créé de manière à ce que la compréhension puisse être atteinte par la conception (même si certains étudiants ne le souhaitent pas ...). C'est précisément ce que Dijkstra voulait dire par "mathématiciens purs" (presque) seulement se préoccuper des faits mathématiques et comprendre leurs propriétés.

Donc, vous ne devriez pas être surpris de produire des preuves correctes est relativement infaillible: c'est le but de tout "l'exercice". (Cela ne signifie pas pour autant que les erreurs n'existent pas ou à peine, l'erreur est humaine, dit-on)

Maintenant, si nous considérons la programmation, quel est notre but? Nous ne cherchons pas vraiment à comprendre, nous voulons quelque chose qui fonctionne . Mais quand quelque chose "fonctionne"? Quelque chose fonctionne quand nous avons réussi à créer quelque chose qui permet à une machine étrange de terminer la tâche que nous voulons qu'elle fasse et de préférence assez rapidement aussi.

C’est là, je crois, la différence fondamentale, car cela signifie que notre objectif ne peut pas simplement être énoncé comme un théorème que notre programme "prouve", nous désirons quelque chose dans le monde réel (quel qu’il soit), pas un artefact mathématique. Cela signifie que nous ne pouvons pas atteindre notre objectif de manière purement théorique (bien que Dijkstra voudrait que vous l'essayiez de manière inconsidérée) car nous devons apaiser la machine, espérons que nous savons réellement quelle tâche nous voulons accomplir et que nous sommes conscients de choses qui n'ont pas été envisagées, mais qui se produisent en quelque sorte.

Donc, à la fin, il n’ya pas d’autre solution que de simplement essayer et probablement échouer, réparer, échouer et réessayer jusqu’à ce que nous soyons quelque peu satisfaits du résultat.

Notez que votre hypothèse consistant à rédiger des preuves sans faille est plus simple que des programmes sans faille (qui sont en fait des déclarations différentes comme le fait remarquer @Ariel ) peuvent en fait être erronés, car les preuves sont souvent construites par essais et erreurs à un certain niveau. Néanmoins, j'espère que cela jette un peu de lumière sur la question implicite: "Quelle est la différence entre prouver un théorème et écrire un programme?" (A quoi un observateur insouciant de la correspondance Curry-Howard pourrait dire: "Rien du tout!")

Comme @wvxvw l'a mentionné dans les commentaires, les paragraphes suivants de «Notes sur la programmation structurée» (EWD249, page 21) sont très pertinents:

(...) Un programme n'est jamais un objectif en soi; le but d'un programme est d'évoquer des calculs et le but de ces calculs est d'établir un effet souhaité. Bien que le programme soit le produit final créé par le programmeur, les calculs possibles évoqués par celui-ci - dont la "confection" est laissée à la machine! - sont le véritable sujet de son métier. Par exemple, chaque fois qu'un programmeur déclare que son programme est correct, il fait une affirmation sur les calculs qu'il peut évoquer.

(...) En un sens, l'élaboration d'un programme est donc plus difficile que celle d'une théorie mathématique: programme et théorie sont des objets structurés et intemporels. Mais alors que la théorie mathématique a un sens en l'état, le programme n'a de sens que par son exécution.

Lamport fournit un motif de désaccord sur la prévalence d'erreurs dans les preuves dans Comment rédiger une preuve (pages 8-9) :

Il y a une vingtaine d'années, j'ai décidé de rédiger une preuve du théorème de Schroeder-Bernstein pour un cours d'introduction aux mathématiques. La preuve la plus simple que j'ai pu trouver était dans le texte classique de Kelley sur la topologie générale. Comme Kelley écrivait pour un public plus sophistiqué, j'ai dû ajouter beaucoup d'explications à sa preuve d'une demi-page. J'avais écrit cinq pages quand j'ai réalisé que la preuve de Kelley était fausse. Récemment, je voulais illustrer une conférence sur mon style de preuve avec une preuve incorrecte convaincante, alors je me suis tourné vers Kelley. Je ne trouvais rien de mal à sa preuve; cela semblait évidemment correct! La lecture et la relecture de la preuve m'ont convaincu que ma mémoire était défaillante ou que j'étais très stupide il y a vingt ans. Néanmoins, la preuve de Kelley était courte et servirait d'exemple, alors j'ai commencé à la réécrire sous forme de preuve structurée.

... Le style a d'abord été appliqué à des démonstrations de théorèmes ordinaires dans un article que j'ai écrit avec Martin Abadi. Il avait déjà écrit des preuves conventionnelles, des preuves suffisantes pour nous convaincre et vraisemblablement les arbitres. En réécrivant les preuves dans un style structuré, nous avons découvert que presque toutes les erreurs étaient graves, même si les théorèmes étaient corrects. Tout espoir que des preuves incorrectes ne conduisent pas à des théorèmes incorrects a été détruit lors de notre prochaine collaboration. Maintes et maintes fois, nous conjecturions et écrivions une esquisse de preuve au tableau - une esquisse qui aurait facilement pu être transformée en une preuve conventionnelle convaincante - pour découvrir, en essayant d'écrire une preuve structurée, que la conjecture était fausse. Depuis lors, je n'ai jamais cru à un résultat sans une preuve minutieuse et structurée.

Une grande différence est que les programmes sont généralement écrits pour fonctionner sur des entrées, alors que les démonstrations mathématiques partent généralement d'un ensemble d'axiomes et de théorèmes connus. Parfois, vous devez couvrir plusieurs cas pour obtenir une preuve suffisamment générale, mais les cas et leur résolution sont explicitement énumérés et la portée du résultat est implicitement limitée aux cas couverts.

Comparez cela avec un programme informatique, qui doit fournir une sortie «correcte» pour une gamme d'entrées possibles. Il est rarement possible d'énumérer toutes les entrées et de toutes les essayer. Pire encore, supposons que le programme interagisse avec un être humain et lui permette de modifier son fonctionnement? Les êtres humains sont notoirement imprévisibles et le nombre d'entrées possibles dans un programme relativement important avec une interaction humaine augmente à un rythme prodigieux. Vous devez essayer de prévoir les différentes manières dont un programme peut être utilisé et essayer de faire en sorte que tous ces cas d'utilisation fonctionnent ou échouent au moins de manière raisonnable, lorsque l'échec est la seule option. Et cela en supposant que vous sachiez même comment cela est supposé fonctionner dans tous ces cas obscurs.

Enfin, un programme volumineux ne peut pas vraiment être comparé à une seule preuve, même complexe. Un programme important ressemble probablement davantage à la collecte et à la révision d’une petite bibliothèque de littérature, dont certaines peuvent comporter des erreurs sur lesquelles vous devez travailler. Pour des programmes plus à l’échelle d’une preuve unique, ce qui pourrait être une petite implémentation d’algorithme, par exemple, des ingénieurs en logiciel expérimentés peuvent les compléter sans faire d’erreurs, en particulier lorsqu’ils utilisent des outils modernes qui empêchent / résolvent les erreurs triviales courantes (comme les fautes d’orthographe). ) qui sont équivalents aux premiers problèmes que vous auriez résolus en relisant.

Ils disent que le problème avec les ordinateurs est qu’ils font exactement ce que vous leur dites.

Je pense que cela pourrait être l'une des nombreuses raisons.

Notez qu'avec un programme informatique, le graveur (vous) est intelligent, mais le lecteur (CPU) est stupide.
Mais avec une preuve mathématique, l'écrivain (vous) est intelligent et le lecteur (relecteur) est également intelligent.

Cela signifie que vous ne pouvez jamais vous permettre d'entrer dans une situation "bien, vous savez ce que je veux dire " avec un ordinateur. Il fait exactement ce que vous lui dites, sans connaître vos intentions.

Par exemple, disons que ceci est une étape dans une preuve:

$x^2+4x+3$$x+3$$x = -3$

La réponse de Yuval, à mon avis, ne dit rien: il semble que vous compariez différents animaux.

$n$$n!$

La vérification des propriétés sémantiques des programmes est indécidable (théorème de Rice) et, de manière analogue, le fait de vérifier si une déclaration dans la logique des prédicats du premier ordre est vraie est également indécidable. Le fait est qu'il n'y a pas de réelle différence de dureté par rapport à la manière dont vous envisagez les problèmes. D'autre part, nous pouvons raisonner sur les propriétés syntaxiques des programmes (compilateurs), ce qui est analogue au fait que nous pouvons vérifier des preuves. Les bugs (le code ne fait pas ce que je veux) sont sémantiques, vous devriez donc les comparer à leur contrepartie correcte.

Je renforcerai Yuval et dirai que des domaines entiers ont grandi avec la motivation d'écrire des preuves mathématiques pouvant être écrites et vérifiées dans un système formel, de sorte que même le processus de vérification n'est pas du tout trivial.

Qu'est-ce qui est si différent à écrire des preuves mathématiques irréprochables et à écrire du code informatique irréprochable qui rend le premier plus lisible que le second?

Je crois que les principales raisons sont l’ impotence (donne les mêmes résultats pour les mêmes entrées) et l’ immutabilité (ne change pas).

Et si une preuve mathématique pouvait donner des résultats différents si elle était lue un mardi ou lorsque l'année avançait de 2000 à 1999? Et si une partie de la preuve mathématique consistait à remonter de quelques pages en arrière, à réécrire quelques lignes et à recommencer à partir de là?

Je suis sûr qu'une telle preuve serait presque aussi sujette aux bogues qu'un segment normal de code informatique.

Je vois aussi d'autres facteurs secondaires:

1. Les mathématiciens sont généralement beaucoup plus instruits avant d’essayer d’écrire une preuve significative / publiable. 1/4 des développeurs professionnels éponyme ont commencé à coder il y a moins de 6 ans (voir le sondage SO 2017 ), mais je suppose que la plupart des mathématiciens ont suivi plus de dix ans d'études en mathématiques.
2. Les preuves mathématiques sont rarement soumises au même niveau de contrôle que le code informatique. Une seule faute de frappe peut / va casser un programme, mais des dizaines de fautes de frappe peuvent ne pas suffire à détruire la valeur d'une preuve (juste sa lisibilité).
3. Le diable est dans les détails et le code informatique ne peut pas ignorer les détails. Les épreuves sont libres de sauter les étapes jugées simples / courantes. Il existe de beaux sucres syntaxiques disponibles dans les langues modernes, mais ils sont codés en dur et assez limités en comparaison.
4. Les mathématiques sont plus anciennes et ont une base / noyau plus solide. Il existe certes une multitude de sous-domaines nouveaux et brillants en mathématiques, mais la plupart des principes fondamentaux sont utilisés depuis des décennies. Cela conduit à la stabilité. D'un autre côté, les programmeurs ne s'entendent toujours pas sur la méthodologie de base du codage (il suffit de poser des questions sur le développement Agile et son taux d'adoption).

Je suis d'accord avec ce que Yuval a écrit. Mais la réponse est beaucoup plus simple: dans la pratique, les ingénieurs n’essaient généralement même pas de vérifier l’exactitude de leurs programmes, ils ne le font tout simplement pas, ils n’écrivent même pas les conditions qui définissent le moment où le programme est correct.

Il y a plusieurs raisons à cela. La première est que la plupart des ingénieurs en logiciel ne possèdent pas les compétences nécessaires pour formuler clairement des problèmes de manière mathématique, ni savoir écrire des preuves de correction.

Une autre est que la définition des conditions de correction pour un système logiciel complexe (spécialement un système distribué) est une tâche très difficile et longue. Ils devraient avoir quelque chose qui semble fonctionner en quelques semaines.

Une autre raison est que l'exactitude d'un programme dépend de nombreux autres systèmes écrits par d'autres qui, encore une fois, n'ont pas de sémantique claire. Il existe une loi de Hyrum qui dit essentiellement que si votre bibliothèque / service a un comportement observable (ne fait pas partie de son contrat), quelqu'un finira par en dépendre. Cela signifie essentiellement que l'idée de développer des logiciels sous forme modulaire avec des contrats clairs comme les lemmas en mathématiques ne fonctionne pas dans la pratique. Cela empire dans les langues dans lesquelles la réflexion est utilisée. Même si un programme est correct aujourd'hui, il risque de tomber en panne dès que quelqu'un procédera à une refactorisation triviale dans l'une de ses dépendances.

Dans la pratique, ils ont généralement des tests. Les tests agissent comme ce qui est attendu du programme. Chaque fois qu'un nouveau bogue est trouvé, ils ajoutent des tests pour le détecter. Cela fonctionne dans une certaine mesure, mais ce n’est pas une preuve de correction.

Lorsque les gens n'ont pas les compétences nécessaires pour définir le correct, ni écrire les programmes corrects, ni attendu à le faire et que le faire est plutôt difficile, il n'est pas surprenant que les logiciels ne soient pas corrects.

Mais notons également qu’à la fin, dans de meilleurs endroits, le génie logiciel se fait par révision du code. C’est l’auteur d’un programme qui doit convaincre au moins une autre personne que le programme fonctionne correctement. C’est l’argument avancé par certains arguments informels de haut niveau. Mais, encore une fois, il n’ya généralement rien qui se rapproche d’une définition claire et rigoureuse de l’exactitude ou d’une preuve d’exactitude.

En mathématiques, on se concentre sur la correction. Dans le développement de logiciels, un programmeur doit se préoccuper de nombreuses choses et il existe des compromis entre eux. Avoir un logiciel sans bug ou même une bonne définition de la correction (avec des exigences changeantes dans le temps) est un idéal, mais il doit être échangé contre d’autres facteurs, et l’un des plus importants est le temps passé à le développer par des logiciels existants. développeurs. Ainsi, dans la pratique, l’objectif et les processus atténuent autant que possible le risque de bogues au lieu de rendre le logiciel exempt de bogues.

Il y a déjà beaucoup de bonnes réponses mais il y a encore plus de raisons pour lesquelles les mathématiques et la programmation ne sont pas les mêmes.

1 Les épreuves mathématiques ont tendance à être beaucoup plus simples que les programmes informatiques. Considérons les premières étapes d’une preuve hypothétique:

Soit a un entier

Soit b un entier

Soit c = a + b

Jusqu'à présent, la preuve est bonne. Faisons-en les premières étapes d’un programme similaire:

Soit a = input ();

Soit b = input ();

Soit c = a + b;

Nous avons déjà une myriade de problèmes. En supposant que l'utilisateur ait réellement saisi un entier, nous devons vérifier les limites. Est -ce un plus grand que -32768 (ou quel que soit le min int sur votre système)? Est-ce un moins de 32767? Maintenant, nous devons vérifier la même chose pour b . Et parce que nous avons ajouté a et b, le programme n’est correct que si a + best supérieur à -32768 et inférieur à 32767. Il s'agit de 5 conditions distinctes qu'un programmeur doit se préoccuper de ce qu'un mathématicien peut ignorer. Le programmeur doit non seulement s’inquiéter pour eux, il doit aussi déterminer ce qu’il faut faire lorsque l’une de ces conditions n’est pas remplie et écrire du code à effectuer selon le choix du lecteur, quelle que soit sa décision. Les maths sont simples. La programmation est difficile.

2 Le questionneur ne dit pas s'il fait référence à des erreurs de compilation ou à des erreurs d'exécution, mais les programmeurs ne se soucient généralement pas des erreurs de compilation. Le compilateur les trouve et ils sont faciles à corriger. Ils sont comme des fautes de frappe. Combien de fois les gens tapent-ils plusieurs paragraphes sans erreur la première fois?

3 Entraînement.Dès le plus jeune âge, on nous apprend à faire des mathématiques et nous sommes confrontés à de nombreuses erreurs mineures. Un mathématicien expérimenté devait commencer à résoudre des problèmes d’algèbre en plusieurs étapes, généralement au collège, et devait en traiter des dizaines (ou plus) chaque semaine pendant un an. Un seul signe négatif abandonné a causé tout un problème. Après l'algèbre, les problèmes sont devenus plus longs et plus difficiles. Les programmeurs, en revanche, ont généralement une formation beaucoup moins formelle. Beaucoup sont autodidactes (du moins au début) et n'ont reçu aucune formation formelle avant l'université. Même au niveau universitaire, les programmeurs doivent suivre pas mal de cours de mathématiques, tandis que les mathématiciens ont probablement suivi un ou deux cours de programmation.

J'aime la réponse de Yuval, mais je voulais en parler un peu. Une des raisons pour lesquelles vous pourriez trouver plus facile d’écrire des preuves en mathématiques pourrait se résumer à la façon dont l’ontologie mathématique platonique est. Pour voir ce que je veux dire, considérons ce qui suit:

• Les fonctions en mathématiques sont pures (le résultat complet de l'appel d'une fonction est entièrement encapsulé dans la valeur de retour, qui est déterministe et calculée intégralement à partir de la valeur d'entrée).
• Math n'a pas de mutation ni de réaffectation (lorsque vous devez modéliser de telles choses, des fonctions et des séquences sont utilisées).
• Les mathématiques sont référentiellement transparentes (par exemple, pas de pointeurs, pas de notion d'appel par nom ou d'appel par valeur) et les objets mathématiques ont une sémantique d'égalité d'extension (si "deux" choses sont identiques de toutes les manières observables, elles le sont en réalité la même chose).

Bien que l'on puisse se demander si les restrictions ci-dessus facilitent la rédaction d' un programme, je pense qu'il est généralement admis que les restrictions ci-dessus facilitent le raisonnement à propos d'un programme. Lorsque vous écrivez une preuve mathématique, la principale chose à faire est de motiver la preuve que vous écrivez actuellement (puisque, contrairement à la programmation, vous ne devez jamais dupliquer l'effort en math, les abstractions étant gratuites), il est généralement intéressant d'insister sur le point. au-dessus des restrictions.

Les preuves mathématiques fondamentales ne constituent pas une application du monde réel, conçue pour répondre aux besoins de l’homme vivant.

Les humains vont changer leurs désirs, leurs besoins et leurs exigences quotidiennement, probablement dans le domaine des programmes informatiques.

Qu'est-ce qui est si différent à écrire des preuves mathématiques irréprochables et à écrire du code informatique irréprochable qui rend le premier plus lisible que le second?

Avec une exigence aussi claire qu'un problème mathématique, un programme sans faille pourrait être écrit. Prouver que l'algorithme de Dijkstra peut trouver le chemin le plus court entre deux points d'un graphe n'est pas la même chose que de mettre en œuvre un programme qui accepte des entrées arbitraires et de rechercher les points les plus courts entre deux points quelconques.

Il y a des problèmes de mémoire, de performances et de matériel à gérer. J'aimerais que nous ne puissions pas penser à cela lors de l'écriture d'algorithmes, que nous puissions utiliser des constructions pures et fonctionnelles pour gérer cela, mais les programmes informatiques vivent dans le "vrai" monde du matériel alors que la preuve mathématique réside dans ... la "théorie".

Ou, pour être plus succinct :

Sous un autre angle, dans un contexte non universitaire, il s'agit souvent d'argent.

Comme les autres publications le disent bien, Math est une spécification abstraite unique. Par conséquent, une preuve doit fonctionner de manière cohérente dans cette spécification uniquement. Un programme informatique peut fonctionner sur de nombreuses implémentations de la spécification abstraite des mathématiques - c’est-à-dire la façon dont un langage ou un fabricant de matériel implémente des mathématiques à virgule flottante peut être légèrement différent d’un autre, ce qui peut entraîner de légères fluctuations dans les résultats.

En tant que tel, "prouver" un programme informatique avant de l'écrire impliquerait alors de prouver la logique au niveau du matériel, du système d'exploitation, du pilote, du langage de programmation, du compilateur, éventuellement d'un interprète, pour chaque combinaison possible de matériel que le programme pourrait éventuellement être utilisé et toutes les données imaginables qu’il pourrait ingérer. Vous trouverez probablement ce niveau de préparation et de compréhension sur les missions spatiales, les systèmes d’armes ou les systèmes de contrôle de l’énergie nucléaire, où échec signifie des dizaines de milliards de dollars perdus et potentiellement de nombreuses vies perdues, mais pas grand-chose.

Pour votre programmeur et / ou entreprise "quotidien", il est bien plus rentable d'accepter un certain niveau de précision dans un code généralement correct et de vendre un produit utilisable, et les développeurs peuvent corriger de manière rétroactive les bogues dès qu'ils sont découverts au cours de son exécution. usage.

Je pense que votre raisonnement est valable, mais votre apport ne l’est pas. Les preuves mathématiques ne sont tout simplement pas plus tolérantes aux fautes que les programmes, si les deux sont écrits par des humains. Dijkstra a déjà été cité ici, mais je vais proposer un devis supplémentaire.

Cependant, nous devons organiser les calculs de manière à ce que nos pouvoirs limités soient suffisants pour garantir que le calcul établira l'effet souhaité. Cette organisation comprend la composition du programme et nous sommes confrontés au prochain problème de taille, à savoir. la longueur du texte du programme, et nous devrions également donner à ce problème une reconnaissance explicite. Nous devons rester conscients du fait que la mesure dans laquelle nous pouvons lire ou écrire un texte dépend beaucoup de sa taille. [...]

C’est dans le même esprit que je voudrais attirer l’attention du lecteur sur le fait que la "clarté" a des aspects quantitatifs prononcés, un fait que beaucoup de mathématiciens, curieusement, semblent ignorer. Un théorème énonçant la validité d'une conclusion lorsque dix pages remplies de conditions sont remplies n'est pas un outil commode, car toutes les conditions doivent être vérifiées chaque fois que le théorème est appelé. En géométrie euclidienne, le théorème de Pythagore est valable pour trois points quelconques A, B et C tels que, par A et C, une ligne droite puisse être tracée orthogonalement à une ligne droite par B et C. Combien de mathématiciens estiment que le théorème reste applicable ou tous les points A, B et C coïncident? cependant, cela semble en grande partie responsable de la commodité avec laquelle le théorème de Pythagore peut être utilisé.

Pour résumer: en tant qu’être humain lent d’esprit, j’ai une très petite tête et je ferais bien d’apprendre à vivre avec elle, à respecter mes limites et à leur rendre pleinement hommage, plutôt que d’essayer de les ignorer, car ce dernier effort vain sera vain. puni par l'échec.

Ceci est légèrement édité les trois derniers paragraphes du premier chapitre de la programmation structurée de Dijkstra.

Pour reformuler peut-être ceci, appliquez mieux à votre question: l'exactitude est en grande partie fonction de la taille de votre preuve. La correction de longues preuves mathématiques est très difficile à établir (beaucoup de "preuves" publiées vivent dans les limbes de l'incertitude puisque personne ne les a réellement vérifiées). Mais, si vous comparez l'exactitude de programmes triviaux à des preuves triviales, il n'y a probablement aucune différence notable. Cependant, les assistants de preuve automatisés (au sens large, votre compilateur Java est également un assistant de preuve), permettent aux programmes de gagner en automatisant de nombreux travaux préparatoires.

Comme d'autres réponses l'ont évoqué (je veux élaborer), mais l'utilisation des bibliothèques est une grande partie du problème. Même avec une documentation parfaite (aussi courante qu'un code sans écriture), il est impossible de transférer la connaissance complète d'une bibliothèque à tous les programmeurs utilisant cette bibliothèque. Si le programmeur ne comprend pas parfaitement sa bibliothèque, il peut faire des erreurs lors de son utilisation. Parfois, cela peut entraîner des bogues critiques qui sont découverts lorsque le code ne fonctionne pas. Mais pour les bugs mineurs, ceux-ci peuvent passer inaperçus.

Une situation similaire serait si un mathématicien utilisait des preuves et des lemmas existants sans les comprendre parfaitement; leurs propres preuves seraient probablement imparfaites. Bien que cela puisse suggérer une solution, il faut apprendre parfaitement toutes les bibliothèques utilisées; cela prend pratiquement beaucoup de temps et peut nécessiter une connaissance du domaine que le programmeur ne possède pas (je connais très peu de choses sur le séquençage de l’ADN / la synthèse de protéines; je peux pourtant travailler avec ces concepts à l’aide de bibliothèques).

De manière plus succincte, l’ingénierie logicielle (l’ingénierie en général) repose sur l’encapsulation de différents niveaux d’abstraction afin de permettre aux utilisateurs de se concentrer sur des domaines plus restreints du problème dans lequel ils se spécialisent. Cela leur permet de développer une expertise dans leur domaine, mais requiert également une excellente communication. entre chaque couche. Lorsque cette communication n'est pas parfaite, cela crée des problèmes.

Je vais essayer d'être original après toutes ces bonnes réponses.

Les programmes sont des preuves

L' isomorphisme de Curry-Howard nous dit, les types dans votre programme sont les théorèmes et le code réel en est la preuve.

Certes, il s'agit d'une vue très abstraite et de haut niveau. Le problème qui vous préoccupe probablement est que l'écriture d'un code typique est plus difficile car il est trop bas. Dans la plupart des cas, vous "devez indiquer à la machine quoi faire". Ou bien, examinons la question sous un autre angle: les mathématiciens sont vraiment bons en abstraction.

Comme note de côté: "La musique des ruisseaux" est l’un des plus beaux ponts entre les deux. Il définit essentiellement des choses pour être en mesure de dire « Je veux ce dans ce sens » et la machine fait par magie ce exactement comme vous le souhaitez.

Aucune des nombreuses autres réponses n'indique ce qui suit. Les preuves mathématiques opèrent sur des systèmes informatiques imaginaires dotés d'une mémoire infinie et d'une puissance de calcul infinie. Ils peuvent donc détenir des nombres arbitrairement grands avec une précision infinie et ne perdre aucune précision dans aucun calcul.

$\pi$

Ce n'est pas. Les preuves mathématiques sont exactement aussi bousculées par nature, c'est simplement que leurs lecteurs sont plus permissifs qu'un compilateur. De la même manière, les lecteurs d’un programme informatique sont facilement persuadés qu’il est correct, du moins jusqu’à ce qu’ils essaient de l’exécuter.

Par exemple, si nous essayons de traduire une preuve mathématique dans un langage formel tel que ZFC, elle contiendra également des bogues. C'est parce que ces preuves peuvent être très longues, nous sommes donc obligés d'écrire un programme pour générer les preuves. Peu de gens vont à la peine, à leurs risques et périls, bien qu'il y ait des recherches actives dans la formalisation des preuves fondamentales.

Et en effet, les mathématiques peuvent obtenir des BSOD! Ce ne serait pas la première fois!

Cette idée orthodoxe que toutes les preuves mathématiques suffisamment vérifiées sont essentiellement correctes ou peuvent être corrigées est la même qui motive votre projet logiciel au travail: tant que nous resterons sur la feuille de route, nous éliminerons tous les bugs et fonctionnalités complètes - il s'agit d'un processus itératif menant à un produit final défini.

Voici le revers. Regardez, nous avons déjà le financement, le concept d'entreprise validé, tous les documents sont ici pour que vous puissiez les lire. Nous avons juste besoin de vous pour exécuter et c'est une chose sûre!

Ne soyons pas trop désolés pour Hilbert non plus, il savait dans quoi il s'embarquait. C'est juste des affaires.

Si vous voulez vraiment en être sûr, prenez tout au cas par cas et tirez vos propres conclusions!

Je vois deux raisons importantes pour lesquelles les programmes sont plus sujets aux erreurs que les épreuves mathématiques:

1: Les programmes contiennent des variables ou des objets dynamiques évoluant dans le temps, alors que les objets mathématiques des épreuves sont généralement statiques. Ainsi, la notation en mathématiques peut être utilisée comme support direct du raisonnement (et si a = b, cela reste le cas) lorsque cela ne fonctionne pas dans les programmes. En outre, ce problème s'aggrave lorsque les programmes sont parallèles ou comportent plusieurs threads.

2: Les mathématiques supposent souvent des objets relativement bien définis (graphes, variétés, anneaux, groupes, etc.) tandis que la programmation traite avec des objets très confus et plutôt irréguliers: arithmétique en précision finie, piles finies, conversions caractère-entier, pointeurs, déchets à collecter , etc ... Il est donc très difficile de garder à l’esprit la collection de conditions pertinentes pour l’exactitude.

Vous devez distinguer deux "catégories" différentes:

• pseudo-preuves (ou pseudo-codes) - c'est ce que vous voyez dans les livres. Il est écrit en langage naturel (par exemple en anglais). C'est ce que vous devriez utiliser pour apprendre les mathématiques (ou les algorithmes).
• preuves formelles (ou code formel) - vous l'écrivez lorsque vous avez besoin que votre preuve (ou code) soit vérifiable mécaniquement (ou exécutable). Une telle représentation ne nécessite aucune "intelligence humaine". Il peut être vérifié (ou exécuté) mécaniquement, en suivant certaines étapes prédéfinies (généralement effectuées par les ordinateurs actuels).

Nous utilisons le pseudo-code depuis des milliers d'années (par exemple, l'algorithme d'Euclids). L'écriture de code formel (dans des langages formels comme C ou Java) est devenue extrêmement populaire et utile après l'invention de l'ordinateur. Malheureusement, les preuves formelles (dans des langages formels tels que Principia Mathematica ou Metamath) ne sont pas très populaires. Et puisque tout le monde écrit des pseudo-preuves aujourd'hui, on se dispute souvent à propos de nouvelles preuves. On peut y trouver des erreurs des années, des décennies, voire des siècles après le "prouver".

Je ne trouve pas la référence, mais je pense que Tony Hoare a déjà dit quelque chose comme suit: La différence entre vérifier un programme et vérifier une preuve est qu’une preuve peut être vérifiée deux lignes à la fois.

En un mot: localité.

Les preuves sont écrites de manière à pouvoir être facilement vérifiées. Les programmes sont écrits pour pouvoir être exécutés. Pour cette raison, les programmeurs laissent généralement de côté les informations utiles à une personne vérifiant le programme.

Considérons ce programme, où x est en lecture seule

    assume x >= 0
    p := 0 ;
    var pp := 0 ;
    while( x >= pp + 2*p + 1 ) 
    {
        var q := 1 ;
        var qq := q ;
        var pq := p ;
        while(  pp + 4*pq + 4*qq <= x )
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Il est facile à exécuter, mais difficile à vérifier.

Mais si je rajoute dans les assertions manquantes, vous pouvez vérifier le programme localement en vérifiant simplement que chaque séquence d’assignations est correcte eu égard à ses pré et post conditions et que, pour chaque boucle, la postcondition de la boucle est implicite invariant et la négation du bouclier.

    assume x >= 0
    p := 0 ;
    var pp := 0 ; 
    while( x >= pp + 2*p + 1 ) 
        invariant p*p <= x 
        invariant pp == p*p
        decreases x-p*p 
    {
        var q := 1 ;
        var qq := q ; 
        var pq := p ; 
        while(  pp + 4*pq + 4*qq <= x )
            invariant (p+q)*(p+q) <= x
            invariant q > 0 
            invariant qq == q*q 
            invariant pq == p*q 
            decreases x-(p+q)*(p+q)
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        assert (p+q)*(p+q) <= x and pp==p*p and pq==p*q and qq==q*q and q>0
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Revenons à la question initiale: pourquoi la rédaction d'épreuves mathématiques est-elle plus fiable que la rédaction de code informatique? Étant donné que les épreuves sont conçues pour être facilement vérifiées par leurs lecteurs, elles sont également vérifiées par leurs auteurs. Par conséquent, les auteurs avertis ont tendance à ne pas faire (ou au moins conserver) des erreurs logiques dans leurs preuves. Lorsque nous programmons, nous échouons souvent à écrire la raison pour laquelle notre code est correct; le résultat est qu'il est difficile à la fois pour les lecteurs et pour l'auteur d'un programme de vérifier le code; le résultat est que les auteurs font (puis gardent) des erreurs.

Mais il y a de l'espoir. Si, lorsque nous écrivons un programme, nous écrivons également la raison pour laquelle nous pensons que le programme est correct, nous pouvons alors vérifier le code au fur et à mesure que nous l'écrivons et écrire ainsi un code moins bogué. Cela présente également l'avantage que d'autres peuvent lire notre code et le vérifier par eux-mêmes.

On pourrait se demander s'il est plus difficile en pratique ou en principe d'écrire des preuves ou d'écrire du code.

En pratique, prouver est beaucoup plus difficile que de coder. Très peu de personnes qui ont suivi deux années de mathématiques au niveau universitaire peuvent écrire des preuves, même triviales. Parmi les personnes qui ont suivi deux années de CS au niveau universitaire, au moins 30% peuvent probablement résoudre FizzBuzz .

Mais en principe , il y a des raisons fondamentales pour lesquelles c'est l'inverse. Au moins en principe, les preuves peuvent être vérifiées par un processus qui ne nécessite ni jugement ni compréhension. Les programmes ne peuvent pas - nous ne pouvons même pas dire, par un processus prescrit, si un programme va s’arrêter.

Seule une petite partie des énoncés mathématiques qui sont vrais peut être prouvée de manière pratique. Plus important encore, il serait impossible de construire un ensemble d'axiomes mathématiques non triviaux (*) permettant de prouver toutes les affirmations vraies. S'il suffisait d'écrire des programmes pour faire une infime fraction de ce que l'on pourrait faire avec un ordinateur, il serait possible d'écrire un logiciel parfaitement correct, mais les ordinateurs sont souvent appelés à faire des choses qui vont au-delà de ce qui est prouvé comme correct le logiciel peut accomplir.

(*) Il est possible de définir un ensemble d'axiomes permettant d'énumérer toutes les déclarations vraies, et donc de les prouver, mais celles-ci ne sont généralement pas très intéressantes. Bien qu'il soit possible de catégoriser formellement des ensembles d'axiomes en ceux qui sont ou non, relativement parlant, non triviaux, le point clé est que l'existence prouvable d'affirmations vraies mais non prouvables n'est pas un défaut dans un ensemble. d'axiomes. Ajouter des axiomes pour rendre prouvables des déclarations vraies mais non démontables ferait en sorte que d'autres déclarations deviennent vraies, mais sans elles.

1. Les programmes informatiques sont testés dans le monde réel. Une erreur technique délicate dans une longue preuve mathématique, que seul un nombre limité de personnes peut comprendre, a de bonnes chances de rester non détectée. Le même type d'erreur dans un produit logiciel est susceptible de produire un comportement étrange que les utilisateurs ordinaires remarquent. Donc, la prémisse pourrait ne pas être correcte.

2. Les programmes informatiques remplissent des fonctions utiles dans le monde réel. Pour ce faire, il n'est pas nécessaire qu'ils soient 100% corrects, et des normes élevées de précision sont assez coûteuses. Les preuves ne sont utiles que si elles prouvent réellement quelque chose. Par conséquent, ignorer la partie "100% correct" n'est pas une option pour les mathématiciens.

3. Les preuves mathématiques sont clairement définies. Si une preuve est erronée, l'auteur a commis une erreur. De nombreux bogues dans les programmes informatiques surviennent parce que les exigences n'ont pas été correctement communiquées ou en raison d'un problème de compatibilité avec quelque chose dont le programmeur n'a jamais entendu parler.

4. De nombreux programmes informatiques ne peuvent pas être prouvés corrects. Ils peuvent résoudre des problèmes définis de manière informelle, tels que la reconnaissance de visages. Ils peuvent aussi ressembler à un logiciel de prévision boursière et avoir un objectif formellement défini, mais impliquent trop de variables du monde réel.

Une grande partie des mathématiques en tant qu'activité humaine consiste à développer des langages spécifiques à un domaine dans lesquels la vérification des preuves est facile à effectuer.

La qualité d'une preuve est inversement proportionnelle à sa longueur et à sa complexité. La longueur et la complexité sont souvent réduites en développant une bonne notation pour décrire la situation sur laquelle nous faisons une déclaration, ainsi que les concepts auxiliaires interagissant dans la preuve particulière considérée.

Ce n'est pas un processus facile, et la plupart des preuves observées par des personnes retirées du champ de la recherche se trouvent dans des domaines mathématiques (comme l'algèbre et l'analyse) qui ont connu des centaines, voire des milliers d'années au cours desquelles la notation de ce domaine a été affiné au point que le fait d’écrire les épreuves ressemble à une brise.

Cependant, à la pointe de la recherche, en particulier si vous travaillez sur des problèmes qui ne sont pas dans des domaines avec une notation bien établie ou bien développée, je parierais que la difficulté de rédiger une preuve correcte se rapproche de la difficulté d'écrire un programme correct. C’est parce que vous devez également écrire en même temps l’analogue d’une conception en langage de programmation, entraîner votre réseau neuronal à le compiler correctement, essayer d’écrire la preuve, manquer de mémoire, essayer d’optimiser le langage, itérez votre cerveau en apprenant la langue, rédigez la preuve, etc.

Pour réitérer, j'estime qu'écrire des preuves correctes peut résoudre la difficulté d'écrire des programmes corrects dans certains domaines des mathématiques, mais ces domaines sont nécessairement jeunes et sous-développés car la notion même de progrès en mathématiques est intimement liée à la facilité de preuve vérification.

Une autre façon de formuler ce que je veux dire est que les langages de programmation et les mathématiques sont conçus à la fin de la journée de sorte que les programmes informatiques et les épreuves puissent être compilés. C’est juste que la compilation d’un programme d’ordinateur se fait sur un ordinateur et assure une correction syntaxique qui a généralement peu à voir avec la correction du programme lui-même, tandis que la "compilation" d’une preuve est effectuée par un humain et garantit la correction syntaxique, ce qui revient au même. exactitude de la preuve.

Vous comparez honnêtement des pommes et des oranges ici. Résistance aux pannes et sans bug ne sont pas la même chose.

Si un programme compare les chiffres 2et 3qu’il le dit 2 is greater than 3, cela peut être dû à une implémentation erronée:

# Buggy implementation
function is_a_greater_than_b(a,b):
  return b > a

Le programme est toujours sans faute cependant. Quand on compare deux nombres aet b, il sera toujours capable de vous dire si best plus grand que le a. Ce n'est tout simplement pas ce que vous (le programmeur) êtes censé demander à l'ordinateur de faire.

a) Parce que les programmes informatiques sont beaucoup plus volumineux que les épreuves mathématiques

a.1) Je crois qu'il y a plus de gens utilisés lors de la rédaction d'un programme informatique complexe que lors de la rédaction d'une preuve mathématique. Cela signifie que la marge d'erreur est plus élevée.

b) Parce que les PDG / Actionnaires se soucient plus de l'argent que de la correction de petits bugs , vous (en tant que développeur) devez vous acquitter de vos tâches pour respecter certaines exigences / échéances / démonstrations

c) Parce que vous pouvez être programmeur sans connaissances approfondies en science-fiction, en attendant, ce serait difficile à faire en mathématiques (je crois)

Aditionellement:

NASA:

Ce logiciel est sans bug. C'est parfait, aussi parfait que les êtres humains ont atteint. Considérez ces statistiques: les trois dernières versions du programme, chacune longue de 420 000 lignes, ne comportaient qu’une seule erreur. Les 11 dernières versions de ce logiciel comportaient un total de 17 erreurs.

Prenez la mise à niveau du logiciel pour permettre à la navette de naviguer avec les satellites de positionnement global, une modification qui implique seulement 1,5% du programme, soit 6 366 lignes de code. Les spécifications de cette modification comportent 2 500 pages, soit un volume plus épais qu'un annuaire téléphonique. Les spécifications du programme actuel couvrent 30 volumes et 40 000 pages.

https://www.fastcompany.com/28121/they-write-right-stuff

Niveaux de base:

Pour les maths, on a:
2 + 3 = 5

J'ai appris cela très tôt. Je peux regarder les éléments les plus fondamentaux: deux objets et trois objets. Génial.

Pour la programmation informatique, la plupart des gens ont tendance à utiliser un langage de haut niveau. Certains langages de haut niveau peuvent même "compiler" dans l'un des langages de bas niveau les plus bas, comme le C. Le C peut ensuite être traduit en langage Assembly. Le langage d'assemblage est ensuite converti en code machine. Beaucoup de gens pensent que la complexité s'arrête là, mais ce n'est pas le cas: les CPU modernes prennent le code machine sous forme d'instructions, mais exécutent ensuite un "micro code" pour exécuter ces instructions.

Cela signifie qu'au niveau le plus élémentaire (traitant des structures les plus simples), nous traitons maintenant du micro-code, qui est incorporé dans le matériel et que la plupart des programmeurs n'utilisent même pas directement, ni ne mettent à jour. En fait, non seulement la plupart des programmeurs ne touchent pas le micro-code (0 niveau supérieur au micro-code), la plupart des programmeurs ne touchent pas le code machine (1 niveau supérieur au micro-code), ni même Assembly (2 niveaux supérieurs au micro-code) ( sauf peut-être pour un peu de formation formelle au collège). La plupart des programmeurs ne passeront plus que trois niveaux ou plus.

En outre, si nous examinons le niveau d’assemblée (le niveau le plus bas généralement atteint par les utilisateurs), chaque étape est compréhensible pour les personnes formées et disposant des ressources nécessaires pour l’interpréter. En ce sens, l'Assemblée est beaucoup plus simple qu'un langage de niveau supérieur. Cependant, Assembly est si simple que la réalisation de tâches complexes, voire médiocres, est très fastidieuse. Les langues de niveau supérieur nous libèrent de cela.

Dans une loi sur le "reverse engineering", un juge a déclaré que, même si le code peut en théorie être traité octet par octet, les programmes modernes impliquent des millions d'octets. un effort pour être réalisable. (Par conséquent, le développement interne n'était pas considéré comme une violation de la règle générale du "copyright de ne pas faire de copies" du droit d'auteur). )

Modernisation:

Vous exécutez du code destiné à 286? Ou utilisez-vous du code 64 bits?

Les mathématiques utilisent des principes fondamentaux qui remontent à des millénaires. Avec les ordinateurs, les gens considèrent généralement que l’investissement dans quelque chose de plus de deux décennies gaspille inutilement des ressources. Cela signifie que les mathématiques peuvent être testées de manière beaucoup plus approfondie.

Normes d'outils utilisés:

On m'a appris (de la part d'un ami ayant une formation en programmation informatique plus formelle que moi) qu'il n'existait pas de compilateur C exempt de bogues répondant aux spécifications C. En effet, le langage C suppose la possibilité d'utiliser une mémoire infinie pour les besoins d'une pile. De toute évidence, une telle exigence impossible a dû être écartée lorsque les gens ont essayé de créer des compilateurs utilisables qui fonctionnent avec des machines réelles, de nature un peu plus finie.

En pratique, j'ai constaté qu'avec JScript dans Windows Script Host, j'ai été capable de réaliser beaucoup de bonnes choses à l'aide d'objets. (J'aime l'environnement, car les outils nécessaires pour essayer du nouveau code sont intégrés aux versions modernes de Microsoft Windows.) Lors de l'utilisation de cet environnement, j'ai constaté qu'il n'existait parfois pas de documentation facile à trouver sur le fonctionnement de l'objet. Cependant, utiliser l'objet est tellement bénéfique que je le fais quand même. Donc, ce que je ferais, c’est écrire du code, ce qui peut être un bug pour un nid de frelons, et le faire dans un environnement bien mis en sandbox où je peux voir les effets et apprendre les comportements de l’objet lorsqu’il interagit avec lui.

Dans d'autres cas, parfois seulement après avoir compris le comportement d'un objet, j'ai constaté que celui-ci (fourni avec le système d'exploitation) présentait un bogue et qu'il s'agissait d'un problème connu que Microsoft a décidé de ne pas résoudre intentionnellement. .

Dans de tels scénarios, est-ce que je me fie à OpenBSD, créé par des programmeurs talentueux qui créent régulièrement de nouvelles versions (deux fois par an), avec un fameux dossier de sécurité de "seulement deux trous distants" sur 10 ans ou plus? (Même s'ils ont des correctifs d'errata pour des problèmes moins graves.) Non, en aucun cas. Je ne compte pas sur un tel produit de qualité aussi élevée, car je travaille pour une entreprise qui prend en charge les entreprises qui fournissent aux utilisateurs des machines utilisant Microsoft Windows. C'est pourquoi mon code doit fonctionner.

La praticité / la facilité d'utilisation exigent que je travaille sur les plates-formes que les utilisateurs trouvent utiles, c'est une plate-forme réputée mauvaise pour la sécurité (même si d'énormes améliorations ont été apportées depuis le début du millénaire et que les produits de la même société étaient bien pires) .

Sommaire

Il y a de nombreuses raisons pour lesquelles la programmation informatique est plus sujette aux erreurs, et cela est accepté par la communauté des utilisateurs d’ordinateurs. En fait, la plupart du code est écrit dans des environnements qui ne tolèrent pas les efforts sans erreur. (Certaines exceptions, telles que l'élaboration de protocoles de sécurité, peuvent nécessiter un peu plus d'effort à cet égard.) Outre les raisons couramment invoquées par les entreprises pour ne pas investir davantage, et le non-respect de délais artificiels pour rendre les clients satisfaits, l'impact de la marche de la technologie qui indique simplement que si vous passez trop de temps, vous travaillerez sur une plate-forme obsolète, car les choses changent de manière significative au cours d'une décennie.

De prime abord, je me souviens avoir été surpris de voir à quel point certaines fonctions très utiles et populaires étaient courtes, lorsque j’ai vu du code source pour strlen et strcpy. Par exemple, strlen peut avoir ressemblé à "int strlen (char * x) {char y = x; while ( (y ++))); return (yx) -1;}"

Cependant, les programmes informatiques typiques sont beaucoup plus longs que cela. En outre, beaucoup de programmes modernes utiliseront un autre code qui pourrait être moins bien testé ou même connu pour être bogué. Les systèmes actuels sont beaucoup plus élaborés que ce qui peut être facilement pensé, sauf en écartant à la main une grande partie de la minutie en tant que "détails traités par des niveaux inférieurs".

Cette complexité obligatoire et la certitude de travailler avec des systèmes complexes, voire erronés, font de la programmation informatique un matériel à vérifier bien plus qu’un grand nombre de mathématiques où les choses ont tendance à se résumer à des niveaux beaucoup plus simples.

Lorsque vous décomposez en mathématiques, vous obtenez des éléments individuels que les enfants peuvent comprendre. La plupart des gens font confiance aux mathématiques; au moins l'arithmétique de base (ou, au moins, compter).

Lorsque vous interrompez vraiment la programmation informatique pour voir ce qui se passe sous le capot, vous vous retrouvez avec des implémentations défectueuses de codes et de codes enfreints exécutés électroniquement, et cette implémentation physique est juste une étape en dessous du microcode dont la plupart des informaticiens formés à l'université n'osez pas toucher (s'ils en sont même conscients).

J'ai parlé à des programmeurs qui sont à l'université ou à des diplômés récents qui s'opposent carrément à l'idée qu'il est possible d'écrire du code sans bug. Ils ont écarté cette possibilité, et bien qu’ils reconnaissent que certains exemples impressionnants (que j’ai pu montrer) sont des arguments convaincants, ils considèrent ces échantillons comme des exemples rares et non représentatifs, tout en écartant la possibilité de pouvoir compter. d'avoir de telles normes plus élevées. (Une attitude très différente de la base beaucoup plus fiable que nous voyons en mathématiques.)

Les preuves mathématiques décrivent "ce que" connaissances et programmes décrivent "comment" savoir ".

L'écriture de programmes est plus complexe car le programmeur doit raisonner sur tous les différents états qui peuvent survenir et sur la manière dont le comportement du programme change. Les preuves utilisent un raisonnement formulé ou catégorique pour prouver des choses concernant d'autres définitions.

La plupart des bogues sont causés par des processus entrant dans des états que le programmeur n'avait pas anticipés. Dans un programme, vous avez généralement des milliers ou, dans un grand système, des millions de variables possibles qui ne sont pas des données statiques, mais qui transforment en réalité le mode d'exécution du programme. Toutes ces interactions créent des comportements impossibles à anticiper, en particulier dans un ordinateur moderne où plusieurs couches d'abstraction changent en dessous de vous.

Dans une preuve, il n'y a pas d'état changeant. Les définitions et les objets de discussion sont fixes. Pour prouver, il faut penser au problème en général et prendre en compte un grand nombre de cas, mais ces cas sont résolus par des définitions.