Types de charge sont souvent annoncés comme un moyen pour vous permettre d'affirmer qu'un programme est correct jusqu'à un cahier des charges. Ainsi, par exemple, il vous est demandé d'écrire un code qui trie une liste - vous êtes en mesure de prouver que le code est correct par codage de la notion de "trier" comme un type, et l'écriture d'une fonction telle que List a -> SortedList a
. Mais comment voulez-vous prouver que le cahier des charges, SortedList
, est-il correct? Ne serait-il pas le cas, le plus complexe de votre cahier des charges est, plus il est probable que votre encodage de cette spécification comme un type est incorrect?
Réponses
Trop de publicités?C'est le statique, type-version du système d', Comment pouvez-vous dire que vos tests sont corrects?
La seule réponse que je peux donner est que, oui, la plus complexe et difficile à manier votre cahier des charges, le plus vous êtes susceptible d'avoir fait une erreur. Vous pouvez gâcher en écrivant quelque chose sur un type de formalisme de la théorie aussi bien que vous le pouvez dans la formalisation de la description de votre programme comme une fonction exécutable.
L'espoir est que votre cahier des charges est simple et assez petit, à en juger par l'examen, alors que votre application qui pourrait être beaucoup plus grande. Il est utile que, une fois que vous avez quelques "graines" idées formalisées, vous pouvez montrer que les idées issues de ces sont corrects. De ce point de vue, plus facilement, vous pouvez mécaniquement et prouvable dériver les pièces de votre cahier des charges à partir des pièces plus simples, et, finalement, de déduire de la mise en œuvre à partir de votre cahier des charges, le plus vous êtes susceptible d'obtenir une mise en œuvre correcte.
Mais il peut être difficile de savoir comment formaliser quelque chose, ce qui a pour effet que vous peut faire une erreur dans la traduction de vos idées dans le formalisme – vous pourriez penser que vous avez prouvé une chose, alors qu'en réalité, vous avez prouvé une autre , ou vous pourriez trouver vous-même faire le type de la théorie de la recherche afin de formaliser une idée.
C'est un problème avec n'importe quel langage de spécification (même l'anglais), pas seulement avec les types dépendants. Votre propre message est un bon exemple: il contient une spécification informelle de "fonction de tri" qui exige uniquement que le résultat soit trié, ce qui n'est pas ce que vous voulez ( \xs -> []
serait admissible). Voir par exemple cet article du blog de Twan van Laarhoven.
Je pense que c'est l'inverse: un bien de type de programme ne peut pas prouver non-sens (en supposant que le système est constistent), tandis que les spécifications peuvent être incompatibles ou tout simplement ridicule. Il n'est donc pas "comment s'assurer que ce morceau de code, qui reflète ma platonicienne des idées?", mais plutôt "comment assurez-vous mes idées de façon significative projet sur le bien-fondé de l'avion de pure règles syntaxiques?". Comment assurez-vous que l'oiseau que vous voyez est un pinson [pour certains fournies notion de mockingbirdness]? Ainsi, l'étude des oiseaux et augmenter vos chances d'avoir raison. Mais comme toujours avec les humains, vous ne pouvez pas être sûr à 100%.
Type de théorie est un moyen d'atténuer l'imperfection de l'esprit humain par l'introduction de règles formelles, la machine-vérifier les preuves (c'est très à papier) et d'autres choses, qui permet de se concentrer et donc à simplifier les problèmes de beaucoup de choses (comme Brouwer a dit: "les Mathématiques n'est rien de plus, rien de moins, que la part exacte de notre pensée"), mais vous ne pouvez pas attendre de n'importe quel outil pour faire de vos pensées "de droite", car il est juste un non uniforme de la notion de justesse. OIE, il n'existe pas de façon formelle connecter formelle et informelle: être informelle, c'est comme être à l'intérieur de l' IO
monade - il n'y a pas d'échappatoire.
Il n'est donc pas "est-ce la syntaxe reflète ma très précise de la sémantique?", mais plutôt "puis-je brancher mon cru sémantique de cette fortement structuré syntaxe?". Les programmes sont propres objets matériels, tandis que les idées sont la lourdeur des approximations, qui peuvent devenir de vraies objets matériels que par convention. Nous avons donc forment une base de l'utilisation des conventions, et alors que nous venons de faire confiance, car il est beaucoup plus judicieux de faire confiance à un petit sous-ensemble de l'ensemble de vos nombreuses idées de tous.
Une chose de méthodes formelles peuvent faire que je ne pense pas que d'autres ont abordé est d'aider à relier les choses simples aux plus complexes. Vous ne pouvez pas savoir à coup sûr de la façon de spécifier exactement comment un Set
structure de données doit comporter, mais si vous pouvez écrire une version simple, basé sur des listes triées, vous pouvez prouver que votre fantaisie version basée sur les arbres de recherche équilibrés rapporte correctement par le biais de l' toList
fonction. Qui est, vous pouvez utiliser des méthodes formelles pour le transfert de votre confiance dans les listes triées à l'équilibre des arbres de recherche.
Comment voulez-vous prouver que les mathématiques sont-elles correctes? C'est, comment voulez-vous prouver que entier plus est la bonne façon de compter les pommes, ou comment voulez-vous prouver que le vrai plus est la bonne façon d'ajouter du poids? Il y a toujours une interface entre le formel et mathématique et l'informel / réel. Il nécessite des compétences et des mathématiques / physique goût à trouver le bon formalisme pour résoudre un problème particulier. Méthodes formelles de ne pas l'éliminer.
La valeur des méthodes formelles est double:
Vous n'allez pas à savoir si votre programme est correct, sauf si vous savez ce que les propriétés qu'elle fait satisfait. Avant de savoir si votre routine de tri est "correct", vous devez d'abord savoir ce qu'il fait réellement. Toute procédure de constatation de l'est va être une méthode officielle (même unité de test!), donc, les gens qui rejettent "méthodes formelles" sont vraiment juste de se limiter à un petit sous-ensemble des méthodes disponibles.
Même lorsque vous savez comment faire pour savoir ce qu'est un programme, les gens font des erreurs dans leur raisonnement mathématique (nous ne sommes pas des créatures raisonnables, ce que certaines idéologies peuvent réclamer); il est donc utile de disposer d'une machine consultez-nous. C'est la même raison pour laquelle nous utilisons des tests unitaires --- c'est agréable de courir d'un bureau vérifiez et assurez-vous que le programme fait ce que nous voulons; mais l'ordinateur ne les vérifier et de nous dire si le résultat est correct aide à prévenir les erreurs. Laisser l'ordinateur vérifiez nos preuves sur le comportement du programme est utile pour exactement la même raison.