Que savons-nous sur les programmes parfaitement corrects?

La complexité croissante des programmes informatiques et la position de plus en plus cruciale des ordinateurs dans notre société me laissent nous demander pourquoi nous n'utilisons toujours pas collectivement des langages de programmation dans lesquels vous devez prouver formellement que votre code fonctionne correctement.

Je crois que le terme est un "compilateur de certification" (je l'ai trouvé ici ): un compilateur compilant un langage de programmation dans lequel il est non seulement nécessaire d'écrire le code, mais aussi d'indiquer la spécification du code et de prouver que le code adhère à la spécification (ou utilisez un prouveur automatique pour le faire).

Lors de mes recherches sur Internet, je n'ai trouvé que des projets utilisant soit un langage de programmation très simple, soit des projets ayant échoué qui tentaient d'adapter les langages de programmation modernes. Cela m'amène à ma question:

Existe-t-il des compilateurs de certification implémentant un langage de programmation complet, ou est-ce très difficile / théoriquement impossible?

De plus, je n'ai encore vu aucune classe de complexité impliquant des programmes prouvables, telle que "la classe de toutes les langues décidables par une machine de Turing pour laquelle il existe une preuve que cette machine de Turing s'arrête", que j'appellerai $ProvableR$ , en tant qu'analogue de $R$ , l'ensemble des langages récursifs.

Je peux voir les avantages d'étudier une telle classe de complexité: par exemple, pour $ProvableR$ le problème Stopper est décidable (je conjecture même définie de la manière évidente serait la plus grande classe de langues pour lesquelles il est décidable). De plus, je doute que nous excluions tous les programmes utiles: qui utiliserait un programme quand on ne peut pas prouver qu'il se termine?$ProvableRE$

Donc ma deuxième question est:

Que savons-nous des classes de complexité qui exigent que leurs langages contenus possèdent certaines propriétés?

"Certifier le compilateur" signifie généralement quelque chose de légèrement différent: cela signifie que vous avez un compilateur qui peut prouver que le code machine qu'il émet correctement implémente la sémantique de haut niveau. C’est-à-dire que c’est la preuve qu’il n’ya pas de bogues de compilation. Les programmes que les utilisateurs donnent au compilateur peuvent toujours être erronés, mais le compilateur générera une version de code machine correcte du mauvais programme. La plus grande réussite de ce type est le compilateur vérifié CompCert , qui est un compilateur pour un grand sous-ensemble de C.

Le compilateur Compcert lui-même est un programme avec une preuve d'exactitude (réalisée en Coq), ce qui garantit que s'il génère du code pour un programme, il sera correct (en ce qui concerne la sémantique opérationnelle d'assembly & C utilisée par les concepteurs CompCert). L'effort de vérification de ces choses est assez grand; En règle générale, la preuve d'exactitude sera comprise entre 1x et 100x la taille du programme que vous vérifiez. Écrire des programmes et des épreuves vérifiés par machine est une nouvelle compétence que vous devez apprendre - ce ne sont pas des mathématiques ou une programmation comme d'habitude, même si cela dépend de la capacité de bien faire les deux. On a l'impression de repartir de zéro, de redevenir un programmeur débutant.

Il n'y a cependant pas d'obstacle théorique particulier à cela. La seule chose qui va dans ce sens est le théorème de Blum Size : pour toute langue dans laquelle tous les programmes sont totaux, vous pouvez trouver un programme dans une langue générale récursive qui sera au moins exponentiellement plus grand une fois programmé dans la langue totale. Pour comprendre ce résultat, une langue totale ne code pas uniquement un programme, mais également une preuve de résiliation. Ainsi, vous pouvez avoir des programmes courts avec des preuves de résiliation longues. Cependant, cela n'a pas vraiment d'importance dans la pratique, car nous n'allons jamais écrire que des programmes avec des preuves de terminaison gérables.

EDIT: Dai Le a demandé quelques précisions sur le dernier point.

Ceci est principalement une affirmation pragmatique, basée sur le fait que si vous pouvez comprendre pourquoi un programme fonctionne, il est alors peu probable que la raison en soit de vastes millions de pages invariantes. (Les invariants les plus longs que j'ai utilisés font quelques pages et font rire les critiques! C'est compréhensible aussi, puisque l'invariant est la raison pour laquelle le programme fonctionne, dépouillé de tout le récit qui aide les gens à le comprendre.)

Mais il y a aussi des raisons théoriques. En gros, nous ne connaissons pas beaucoup de façons d’inventer systématiquement des programmes dont les preuves de correction sont très longues. La méthode principale consiste à (1) prendre la logique dans laquelle vous apportez la preuve de la correction, (2) trouver une propriété qui ne peut pas être directement exprimée dans cette logique (les preuves de cohérence sont la source typique), et (3) trouver un programme dont La preuve de correction repose sur une famille de conséquences exprimables de la propriété inexprimable. Parce que (2) est inexprimable, cela signifie que la preuve de chaque conséquence exprimable doit être effectuée de manière indépendante, ce qui vous permet d'exploser la taille de la preuve de correction. Comme exemple simple, notez que dans la logique du premier ordre avec une relation parent, vous ne pouvez pas exprimer la relation ancêtre.$k$$k$) est exprimable, pour chaque fixé . Ainsi, en donnant un programme qui utilise certaines propriétés d'ascendance jusqu'à une certaine profondeur (par exemple, 100), vous pouvez forcer une preuve d'exactitude dans FOL à contenir cent fois les preuves de ces propriétés.$k$

Le point de vue sophistiqué sur ce sujet est appelé "mathématiques inversées" et consiste à étudier quels axiomes sont nécessaires pour prouver des théorèmes donnés. Je ne sais pas grand chose à ce sujet, mais si vous posez une question sur son application à CS, et je suis sûr qu'au moins Timothy Chow, et probablement plusieurs autres personnes, pourront vous dire des choses intéressantes.

Je pense que la réponse à la première question est qu’en général, c’est trop de travail avec les outils actuels. Pour en comprendre le sens, je suggère d'essayer de prouver l'exactitude de Bubble Sort dans Coq (ou, si vous préférez, un peu plus de défi, utilisez Tri rapide). Je ne pense pas qu'il soit raisonnable de s'attendre à ce que les programmeurs écrivent des programmes vérifiés tant que prouver l'exactitude de tels algorithmes de base est si difficile et prend beaucoup de temps.

Cette question revient à demander pourquoi les mathématiciens n'écrivent pas de preuves formelles vérifiables par des vérificateurs de épreuves. Écrire un programme avec une preuve formelle d’exactitude signifie prouver un théorème mathématique sur le code écrit, et la réponse à cette question s’applique également à votre question.

Cela ne signifie pas qu'il n'y a pas eu de cas réussis de programmes vérifiés. Je sais qu'il existe des groupes qui prouvent le bien-fondé de systèmes tels que l'hyperviseur de Microsoft . Un cas connexe est le compilateur C vérifié de Microsoft . Mais en général, les outils actuels ont besoin de beaucoup de développement (y compris leurs aspects SE et HCI) avant de devenir utiles pour les programmeurs généraux (et les mathématiciens).

En ce qui concerne le dernier paragraphe de la réponse de Neel sur la croissance de la taille du programme pour les langues ne comportant que des fonctions totales, il est en fait facile de prouver encore plus (si j'ai bien compris). Il est raisonnable de s’attendre à ce que la syntaxe de tout langage de programmation soit identique à celle de l’ensemble des fonctions calculables. Ainsi, pour tout langage de programmation où tous les programmes sont complets, il existe une fonction totale calculable qui ne peut être calculée par aucun programme ( de toute taille) dans cette langue.

Pour la deuxième question, j'ai déjà répondu à une question similaire sur le blog de Scott. Fondamentalement, si la classe de complexité a une belle caractérisation et peut être représentée de manière calculable (c'est-à-dire ce que c'est), nous pouvons alors prouver que certaines représentations des problèmes de la classe de complexité sont manifestement totales dans une théorie très faible correspondant à la classe de complexité. L’idée de base est que les fonctions prouvables de la théorie contiennent toutes les et un problème qui est A C $AC^0$$AC^0$-complete pour la classe de complexité, elle contient donc tous les problèmes de la classe de complexité et peut prouver la totalité de ces programmes. La relation entre les preuves et la théorie de la complexité est étudiée dans la complexité des preuves, voir le livre récent de SA Cook et P. Nguyen " Fondements logiques de la complexité de la preuve " si vous êtes intéressé. (Un brouillon de 2008 est disponible.) La réponse de base est donc que pour beaucoup de classes "Provably C = C".

Ce n'est pas vrai en général car il existe des classes de complexité sémantique qui ne possèdent pas de caractérisation syntaxique, par exemple des fonctions calculables totales. Si, par récursif, vous entendez des fonctions récursives totales, alors les deux ne sont pas égaux et l'ensemble des fonctions calculables qui sont vraisemblablement totales dans une théorie est bien étudié dans la littérature sur la théorie de la preuve et sont appelées les fonctions prouvables totales de la théorie. Par exemple: les fonctions prouvables de sont des fonctions récursives ϵ 0 (ou des fonctions équivalentes dans le système T de Godel ), les fonctions prouvables de$PA$$\epsilon_0$$T$ sont fonctionnelles dans le système F de Girard, les fonctions prouvables de total$PA^2$$F$ sont des fonctions récursives primitives, ....$I\Sigma_1$

Mais il ne me semble pas que cela signifie beaucoup dans le contexte de la vérification de programme, car il existe également des programmes qui calculent par extension la même fonction, mais nous ne pouvons pas prouver que les deux programmes calculent la même fonction, c'est-à-dire que les programmes sont par extension égaux mais non intentionnellement. (Cela ressemble à l’Étoile du matin et à l’Étoile du soir.) En outre, il est facile de modifier un programme total vérifiable pour en obtenir un dont la théorie est incapable de prouver sa totalité.

Je pense que les deux questions sont liées. L'objectif est d'obtenir un programme vérifié. Un programme vérifié signifie que le programme satisfait à une description, qui est un énoncé mathématique. Une solution consiste à écrire un programme dans un langage de programmation, puis à en prouver les propriétés, comme il satisfait à la description, ce qui est la pratique la plus courante. Une autre option consiste à essayer de prouver l'énoncé mathématique décrivant le problème à l'aide de moyens restreints, puis à en extraire un programme vérifié. Par exemple, si nous prouvons dans la théorie correspondant à que pour un nombre donné n, il existe une suite de nombres premiers dont le produit est égal à n , alors nous pouvons extraire un $P$$n$$n$$P$algorithme de factorisation à partir de la preuve. (Il existe également des chercheurs qui tentent d’automatiser autant que possible la première approche, mais la vérification des propriétés non triviales intéressantes des programmes est difficile en termes de calcul et ne peut pas être entièrement vérifiée sans faux positifs et négatifs.)

Ce que vous demandez dans la première question est parfois appelé un "compilateur de vérification", et il y a quelques années, Tony Hoare l'avait présenté comme un défi de taille pour la recherche informatique . Dans une certaine mesure, cela existe déjà et est activement utilisé dans des outils tels que le prouveur de théorèmes de Coq , qui organisent le problème par le biais de la théorie des types et du principe de propositions sous forme de types (" Curry-Howard ").

EDIT: je voulais juste mettre l'accent sur "dans une certaine mesure". Ce problème est loin d’être résolu, mais le succès de Coq laisse espérer que ce n’est pas une chimère.

Un outil qui vérifie si un programme est correct est parfois appelé un vérificateur de programme. Dans ce contexte, "correct" signifie généralement deux choses: que le programme ne génère jamais certaines sorties (pensez à une erreur de segmentation, NullPointerException, etc.) et que le programme est conforme à une spécification.

Le code et la spécification peuvent concorder et être perçus comme erronés. En un sens, demander aux développeurs d’écrire des spécifications revient à demander à deux développeurs de résoudre le problème. Si les deux implémentations sont d’accord, vous avez alors une plus grande confiance dans leur acceptation. Dans un autre sens, cependant, les spécifications valent mieux qu'une seconde implémentation. Parce que la spécification n'a pas besoin d'être efficace ni même exécutable, elle peut être beaucoup plus succincte et donc plus difficile à se tromper.

Compte tenu de ces avertissements, je vous recommande de consulter le vérificateur de programme Spec # .

Dans le cas général, il est impossible de créer un algorithme qui confirme si un algorithme est équivalent à une spécification. Ceci est une preuve informelle:

Presque tous les langages de programmation sont Turing-complete. Par conséquent, toute langue choisie par une MT peut également l'être par un programme écrit dans cette langue.

$Equivalence/TM$

$Equivalence/TM$$Non-emptiness/TM$$Emptiness/TM$$Emptiness/TM$$Equivalence/TM$$Equivalence/TM$est également inacceptable. Par conséquent, vous pouvez utiliser un algorithme, que deux machines ne soient pas équivalentes ou non, mais vous ne pouvez pas savoir si elles sont équivalentes ou si vous n'avez pas donné à votre algorithme suffisamment de temps.

Cependant, ce n'est que pour le cas général. Il est possible que vous puissiez décider si les spécifications sont équivalentes au programme, en résolvant une version plus détendue du problème. Par exemple, vous pouvez n’examiner que plusieurs entrées ou dire que les deux programmes sont équivalents avec une certaine incertitude. C’est ce que sont les tests logiciels.

Pour le reste de vos questions:

Remarque: cette partie a été modifiée pour clarification. Il se trouve que j'ai commis l'erreur que j'essayais d'éviter, désolé.

$TrueR$$TrueR \subseteq R$

$ProvableR = TrueR$$ProvableR \subset TrueR$$TrueR \subset ProvableR$. La preuve est très simple: laissez$A \epsilon TrueR$. Par définition, dans chaque entrée$A$renvoie OUI ou NON. Par conséquent,$A$s'arrête à chaque entrée. Il s'ensuit que$A \epsilon ProvableR$ .

De manière informelle, ceci peut être résumé comme suit: Vous ne savez pas qu’une langue est décidable tant que vous n’avez pas prouvé qu’elle est. Donc, si dans un système formel vous avez la connaissance qu'une langue est décidable, cette connaissance peut également servir de preuve à cela. Par conséquent, vous ne pouvez pas savoir simultanément qu’une langue est décidable et qu’elle ne peut pas être prouvée. Ces deux déclarations s’excluent mutuellement.

Mon dernier point est que notre connaissance est partielle et que la seule façon d'étudier $R$ est à travers $ProvableR$. La distinction peut avoir un sens en mathématiques et nous pouvons le reconnaître, mais nous ne possédons aucun outil pour l’étudier. Puisque$ProvableR \subset R$ , nous sommes tenus de ne jamais savoir complètement $R$ dans son intégralité.

@Kaveh résume bien ce qui suit: L'expression «prouvable» signifie toujours prouvable dans un système / théorie donné et ne correspond pas à la vérité en général.

Il en va de même pour toute autre classe de complexité: pour déterminer l’appartenance, vous devez d’abord une preuve. C'est pourquoi je pense que votre deuxième question est trop générale, car elle contient non seulement la théorie de la complexité, mais également la théorie des calculs, en fonction de la propriété que vous souhaitez que le langage ait.

La monographie classique suivante étudie presque exactement votre deuxième question:

Hartmanis, J. Calculs réalisables et propriétés de complexité prouvables , Série de conférences régionales CBMS-NSF en mathématiques appliquées, 30. Société de mathématiques industrielles et appliquées (SIAM), Philadelphie, Pennsylvanie, 1978.

Par exemple, il définit la classe "F-TIME [T (n)]" (où F est un système de preuve formelle raisonnable) comme étant $\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$ (où $M_i$ est la i-ème machine de Turing dans une liste complète de MT, et $T_i(n)$ est la durée maximale de $M_i$ sur les entrées de longueur $n$). Let me just highlight a few results relevant to your question - many more can be found in the monograph and references therein:

Cor. 6.4: Let $T(n) \geq n \log(n)$ be a computable function, and let $g(n) \geq 1$ be an unbounded computable function. Then $F$-$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$.

Theorem 6.5: There exist computable monotonically increasing time bounds $T(n)$ for which $F$-$TIME[T(n)] \neq TIME[T(n)]$.

Theorem 6.14: For any computable $T(n) \geq n \log(n)$, $TIME[T(n)] = \{ L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)] \}$.

For space, however, the situation is better controlled:

Theorem 6.9: (1) If $s(n) \geq n$ is space-constructible, then $SPACE[s(n)] = F$-$SPACE[s(n)]$.

(2) If $SPACE[S(n)]=F$-$SPACE[S(n)]$ ($S(n) \geq n$) alors il y a un espace-constructible $s(n)$ tel que $SPACE[S(n)]=SPACE[s(n)]$.

La question doit être posée correctement. Par exemple, personne ne veut jamais savoir si un programme réel achèverait une mémoire infinie et un moyen de l’accéder (par exemple, une opération permettant de déplacer l’adresse de base d’un nombre). Le théorème de Turing n'a aucune pertinence concrète pour le programme correct et les personnes qui le citent comme un obstacle à la vérification du programme confondent deux choses très différentes. Lorsque les ingénieurs / programmeurs parlent d'exactitude de programme, ils veulent en savoir plus sur les propriétés finies. Ceci est également vrai pour les mathématiciens qui souhaitent savoir si quelque chose est prouvable. La lettre de Godel http://vyodaiken.com/2009/08/28/godels-lost-letter/ l' explique en détail.

Cela signifierait évidemment que, malgré l’indécidabilité du problème d’Entscheidungs, le travail mental d’un mathématicien concernant les questions du type oui ou non pourrait être complètement remplacé par une machine. Après tout, il faudrait simplement choisir le nombre naturel n si grand que, lorsque la machine ne donne pas de résultat, il n’a aucun sens de réfléchir davantage au problème.

Il peut être impossible d’examiner l’immense ensemble d’états d’un programme s’exécutant sur un ordinateur réel et de détecter les mauvais états. Il n’existe aucune raison théorique pour ne pas le faire. En fait, beaucoup de progrès ont été accomplis dans ce domaine - par exemple, voir http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf (merci à Neil Immerman pour me parler de ça)

Un problème différent et plus difficile consiste à spécifier exactement les propriétés qu'un programme doit avoir pour être correctes.