Y a-t-il des langues du monde réel prouvables? (Scala?)

StackOverflow https://stackoverflow.com/questions/4065001

Était-ce utile?

La solution

Oui, il y a des langues conçus pour l'écriture de logiciels prouvable correct. Certains sont même utilisés dans l'industrie. est probablement l'exemple le plus important. J'ai parlé à quelques personnes à Praxis Critical Systems Limited qui l'ont utilisé pour exécuter du code sur Boings (pour la surveillance du moteur) et il semble tout à fait agréable. (Voici un résumé .) Ce système linguistique et la preuve d'accompagnement utilise la seconde technique décrite ci-dessous. Il ne supporte même pas l'allocation de mémoire dynamique!

Mon impression et l'expérience est qu'il ya deux techniques pour la rédaction d'un logiciel correct:

Notez que les deux approches charnières sur le fait que vous avez une spécification formelle à la main (sinon comment voulez-vous dire ce qui est un comportement correct / incorrect), et une sémantique formelle définie de la langue (comment seriez-vous d'autre en mesure de dire ce que le comportement réel de votre programme).

Voici quelques autres exemples d'approches formelles. Si elle est « monde réel » ou non, dépend de qui vous demandez: -)

Je ne connais qu'un seul "correct prouvable" langue application web : UR . Un Ur-programme « passe par le compilateur » est garantie pas:

  • Souffrent de toutes sortes d'attaques par injection de code
  • Retour invalide HTML
  • contiennent des liens intra-applications mortes
  • discordances avoir entre les formulaires HTML et les champs attendus par leurs gestionnaires
  • Inclure le code côté client qui fait des hypothèses erronées sur les services -style « AJAX » que le serveur Web distant fournit
  • Tentative non valide les requêtes SQL
  • Utiliser un marshaling incorrect ou unmarshaling en communication avec les bases de données SQL ou entre les navigateurs et les serveurs Web

Autres conseils

Pour répondre à cette question, vous avez vraiment besoin de définir ce que vous entendez par « démontrable ». Comme Ricky a souligné, toute langue avec un système de type est une langue avec un système de preuve intégré qui fonctionne à chaque fois que vous compilez votre programme. Ces systèmes de preuve sont presque toujours malheureusement impuissants - répondre à des questions comme String vs Int et d'éviter des questions comme « la liste triée? » - mais ils sont des systèmes preuve cependant pas le moins

.

Malheureusement, plus sophistiqué vos objectifs preuve, plus il est difficile de travailler avec un système qui permet de vérifier vos preuves. Ce dégénère assez rapidement dans indécidabilité si l'on considère la taille de la classe des problèmes qui sont indécidables sur les machines de Turing. Bien sûr, vous pouvez théoriquement faire des choses de base comme prouvant l'exactitude de votre algorithme de tri, mais rien de plus que cela va être marcher sur la glace très mince.

Même pour prouver quelque chose comme simple l'exactitude d'un algorithme de tri nécessite un système de preuve relativement sophistiqué. (Note: puisque nous avons déjà établi que les systèmes de type sont un système de preuve construit dans la langue, je vais parler de choses en termes de théorie de type, plutôt que agitant mes mains encore plus vigoureusement) Je suis assez certain que la preuve complète de la décision correcte sur la liste de tri nécessiterait une forme de types dépendants, sinon vous avez aucun moyen de référencer les valeurs relatives au niveau du type. Cela commence immédiatement par effraction dans des domaines de la théorie des types qui ont été présentés indécidable. Ainsi, alors que vous pourriez être en mesure de prouver la justesse de votre liste algorithme de tri, la seule façon de le faire serait d'utiliser un système qui vous permettra également d'exprimer des preuves qui ne peut pas vérifier. Personnellement, je trouve cela très déconcertant.

Il y a aussi l'aspect facilité d'utilisation que je faisais allusion plus haut. Le système de type plus sophistiqué, moins il est agréable à utiliser. Ce n'est pas une règle stricte et rapide, mais je pense qu'il est vrai pour la plupart. Et comme avec tout système formel, vous trouverez souvent que l'expression de la preuve est plus de travail (et plus d'erreurs) que la création de la mise en œuvre en premier lieu.

Avec tout cela de la route, il convient de noter que le système de type Scala (comme Haskell de) est Turing complet, ce qui signifie que vous pouvez théoriquement utiliser pour prouver une propriété décidable votre code, à condition que vous avez écrit votre code façon telle qu'elle se prête à de telles preuves. Haskell est presque certainement une meilleure langue pour ce que Java (depuis la programmation au niveau du type dans Haskell est similaire à Prolog, tandis que la programmation au niveau du type à Scala est plus similaire à SML). Je ne conseille pas que vous utilisez des systèmes de type Scala ou pour de Haskell de cette façon (preuves formelles de correction algorithmique), mais l'option est théoriquement disponible.

Au total, je pense que la raison pour laquelle vous ne l'avez pas vu des systèmes formels dans le « monde réel » découle du fait que les systèmes de preuve formelle ont cédé à la tyrannie impitoyable du pragmatisme. Comme je l'ai mentionné, il y a tant d'efforts impliqués dans l'élaboration de vos preuves exactitude que c'est presque jamais la peine. L'industrie a décidé depuis longtemps qu'il était plus facile de créer des tests ad hoc qu'il devait passer par toute sorte de processus de raisonnement formel d'analyse.

langues typées prouvent l'absence de certaines catégories de faute. Le plus avancé du système de type, plus les fautes qu'ils peuvent prouver l'absence de.

Pour preuve qu'un programme fonctionne ensemble, oui, vous faites un pas en dehors des limites des langues ordinaires, où les mathématiques et la programmation se rencontrent, se serrent la main et de procéder ensuite à parler en utilisant des symboles grecs sur la façon dont les programmeurs ne peuvent pas gérer la Grèce symboles. C'est au sujet de la Σ de toute façon.

Vous posez une question beaucoup d'entre nous ont demandé au fil des ans. Je ne sais pas que j'ai une bonne réponse, mais voici quelques morceaux:

  • Il y a bien compris langues avec la possibilité d'être éprouvée en usage aujourd'hui; Lisp via ACL2 est l'un, et bien sûr le schéma a une définition formelle bien compris ainsi.

  • un certain nombre de systèmes ont essayé d'utiliser les langages fonctionnels purs, ou les presque purs, comme Haskell. Il y a un peu de travail équitable des méthodes formelles dans Haskell.

  • Pour en revenir plus de 20 ans, il y avait une chose de courte durée pour l'utilisation de l'épreuve à la main d'un langage formel qui a ensuite été rigoureusement traduit en un langage compilé. Quelques exemples étaient logiciels d'IBM Cleanroom, ACL, Gypsy et Rose de Computational Logic, John McHugh et de mon travail sur la compilation de confiance de C, et mon propre travail sur l'épreuve à la main pour la programmation des systèmes C. Tous ces obtenu une certaine attention, mais aucun d'entre eux a fait beaucoup dans la pratique.

Une question intéressante à poser, je pense, est ce qui des conditions suffisantes être d'obtenir des approches formelles dans la pratique? J'aimerais entendre quelques suggestions.

Vous pouvez enquêter sur purement langages fonctionnels comme Haskell, qui sont utilisés lorsque l'un de vos besoins est prouvabilité .

Cette est amusant de lire si vous êtes intéressé sur les langages de programmation fonctionnelle et pur langages de programmation fonctionnelle.

utilisations réelles de ces langues prouvables serait incroyablement difficile à écrire et comprendre afterwoods. le monde des affaires a besoin d'un logiciel de travail, rapide.

« prouvable » langues échelle pour l'écriture juste ne pas / la lecture d'un grand prix de base de code du projet et ne semblent fonctionner dans les petites et les cas d'utilisation isolés.

Je suis impliqué dans deux langues prouvables. La première est la langue prise en charge du développeur parfait, un système pour spécifier Sotfware, le raffinage et la génération de code. Il a été utilisé pour certains grands systèmes, y compris lui-même PD, et il est enseigné dans plusieurs universités. La deuxième langue démontrable je suis impliqué est un sous-ensemble prouvable de MISRA-C, voir C / C ++ vérification Blog plus.

Scala est censé être « monde réel », donc aucun effort n'a été fait pour le rendre démontrable. Qu'est-ce que vous pouvez faire à Scala est de produire du code fonctionnel. code fonctionnel est beaucoup plus facile à tester, ce qui est à mon humble avis un bon compromis entre le « monde réel » et prouvable.

EDIT ===== Suppression de mes idées erronées au sujet ML être « prouvable ».

Mon (controversé) définition du « monde réel » dans le contexte du code prouvable correcte est:

  • Il doit impliquer un certain degré de automatisation , sinon vous allez passer beaucoup trop proving beaucoup de temps et de traiter avec des détails peu en désordre, et il va être totalement impraticable (sauf peut-être pour le contrôle des engins spatiaux logiciels et ce genre de chose, pour laquelle vous voudrez peut-être en fait passer megabucks sur des contrôles méticuleux).
  • Il doit prendre en charge un certain degré de programmation fonctionnelle , qui vous aide à écrire du code qui est très modulaire, réutilisable et plus facile à raisonner sur. Il est évident que la programmation fonctionnelle n'est pas nécessaire pour écrire ou prouver Bonjour tout le monde, ou une variété de programmes simples, mais à un certain point, la programmation fonctionnelle ne devient très utile.
  • Bien que vous ne devez pas nécessairement être en mesure d'écrire votre code dans un langage de programmation grand public, comme alternative, vous devriez au moins être en mesure de machine à traduire votre code dans le code raisonnablement efficace écrit dans un langage de programmation grand public, de manière fiable.

Les exigences ci-dessus sont relativement plus universelles. D'autres, comme la capacité à modéliser le code impératif, ou la capacité de prouver des fonctions d'ordre supérieur corriger, peut être important ou essentiel pour certaines tâches, mais pas tous.

Compte tenu de ces points, la plupart des outils répertoriés dans ce billet de blog de la mine peut être utile - bien qu'ils soient presque tous soit nouvelle et expérimentale, ou peu familiers à la grande majorité des programmeurs de l'industrie. Il existe des outils très mature couvert, là cependant.

Qu'en est- Idris et Agda ? Assez vrai monde?

Comme un bon exemple de la vie réelle, il y a un projet qui vise à fournir une bibliothèque HTTP REST vérifiée écrit en Agda, appelé Lemmachine:

Non affilié à StackOverflow
scroll top