Afin de répondre à cette question, vous avez vraiment besoin de définir ce que vous entendez par "prouvable". Comme Ricky l'a souligné, n'importe quelle langue avec un système de type est une langue avec un système de preuves qui s'exécute chaque fois que vous compilez votre programme. Ces systèmes d'épreuves sont presque toujours malheureusement impuissant — répondre à des questions comme String vs Int et en évitant des questions comme "est la liste triée?" — mais ils sont la preuve des systèmes d'aucun-le-moins.
Malheureusement, le plus sophistiqué de votre preuve objectifs, plus il est difficile de travailler avec un système qui permet de vérifier vos preuves. Cela dégénère assez rapidement dans l'indécidabilité lorsque l'on considère la taille de la classe de problèmes qui sont indécidable sur des Machines de Turing. Bien sûr, vous pouvez théoriquement faire des choses de base comme le prouve la justesse de votre algorithme de tri, mais rien de plus que cela va être de marcher sur de la glace très fine.
Même pour prouver quelque chose de simple comme la correction d'un algorithme de tri nécessite un niveau relativement sophistiqué système de preuves. (remarque: puisque nous avons déjà établi que les systèmes de type sont une preuve de système intégré dans la langue, je vais vous parler de choses en termes de théorie des types, plutôt que d'en agitant mes mains encore plus vigoureusement) je suis assez certain qu'une preuve de correction sur la liste du tri aurait besoin de certains types de charge, sinon vous n'avez aucune façon de référencer les valeurs relatives au niveau du type. Cela commence tout de suite à la rupture dans les domaines de la théorie des types qui ont été montré pour être 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 les preuves dont il ne peut pas vérifier. Personnellement, je trouve cela très troublant.
Il y a aussi la facilité d'utilisation, aspect auquel je faisais allusion plus haut. Le plus sophistiqué de votre type de système, le moins agréable à l'utilisation. Ce n'est pas une règle dure et rapide, mais je pense que c'est vrai pour la plupart. Et comme avec tout système formel, vous trouverez souvent que le fait d'exprimer la preuve, c'est plus de travail (et de plus en plus enclins à faire des erreurs) que la création de la mise en œuvre en premier lieu.
Avec tout ça de la manière, il est intéressant de noter que la Scala du type de système (comme Haskell) est Turing Complet, ce qui signifie que vous pouvez théoriquement l'utiliser pour prouver tout decidable de propriété sur votre code, à condition que vous avez écrit votre code de telle façon qu'il se prête à de telles épreuves. Haskell est presque certainement un meilleur langage pour ce que Java (depuis le niveau du type de programmation en Haskell est similaire à Prolog, tandis que le type de programmation au niveau de la Scala est de plus en plus semblables à SML). Je ne conseille pas que vous utilisez Scala ou Haskell type de systèmes dans cette voie (de preuves formelles de l'algorithmique de justesse), mais l'option est théoriquement disponible.
Tout à fait, je pense que la raison pour laquelle vous n'avez pas vu systèmes formels dans le "monde réel" provient du fait que la preuve formelle de systèmes ont cédé à l'impitoyable tyrannie du pragmatisme. Comme je l'ai mentionné, il y a donc beaucoup d'efforts impliqués dans l'élaboration de votre exactitude des preuves que ce n'est presque jamais la peine. L'industrie a décidé il y a longtemps qu'il était plus facile de créer ad hoc sur les tests qu'il était de passer par toute sorte d'analyse formelle des processus de raisonnement.
