Чтобы ответить на этот вопрос, вам действительно нужно определить, что вы подразумеваете под "доказуемым". Как указывал Рики, любой язык с системой типов - это язык со встроенной системой проверки, которая запускается каждый раз, когда вы компилируете свою программу. Эти системы доказательств почти всегда печально бессильны & mdash; отвечая на вопросы типа String против Int и избегая вопросов типа "список отсортирован?" & Mdash; но тем не менее они являются системами доказательств.
К сожалению, чем сложнее ваши цели доказательств, тем сложнее работать с системой, которая может проверять ваши доказательства. Это довольно быстро перерастает в неразрешимость, если учесть огромный размер класса проблем, неразрешимых на машинах Тьюринга. Конечно, теоретически вы можете делать базовые вещи, такие как доказательство правильности вашего алгоритма сортировки, но все, что угодно, будет идти по очень тонкому льду.
Даже для доказательства чего-то простого, например, правильности алгоритма сортировки, требуется сравнительно сложная система доказательств. (примечание: поскольку мы уже установили, что системы типов являются системой доказательств, встроенной в язык, я собираюсь поговорить о вещах в терминах теории типов, а не махать руками еще более энергично) Я вполне уверен, что для полной корректности сортировки списка потребуется некоторая форма зависимых типов, в противном случае у вас нет возможности ссылаться на относительные значения на уровне типа. Это немедленно начинает распадаться на сферы теории типов, которые оказались неразрешимыми. Таким образом, хотя вы можете доказать правильность алгоритма сортировки списков, единственный способ сделать это - использовать систему, которая также позволит вам выдвигать доказательства, которые он не может проверить. Лично меня это очень смущает.
Существует также аспект простоты использования, о котором я упоминал ранее. Чем сложнее ваша система типов, тем менее приятным является ее использование. Это не жесткое и быстрое правило, но я думаю, что оно справедливо по большей части. И, как и в любой формальной системе, вы часто обнаруживаете, что выражение доказательства является более трудоемким (и более подверженным ошибкам), чем создание реализации в первую очередь.
Несмотря на все это, стоит отметить, что система типов Scala (например, Haskell) является Turing Complete, что означает, что вы можете теоретически использовать ее для доказательства любого разрешимого свойства вашего кода, что вы написали свой код таким образом, что он поддается таким доказательствам. Haskell почти наверняка является лучшим языком для этого, чем Java (поскольку программирование на уровне типов в Haskell похоже на Prolog, тогда как программирование на уровне типов в Scala больше похоже на SML). Я не советую вам использовать системы типов Scala или Haskell таким образом (формальные доказательства алгоритмической корректности), но эта опция теоретически доступна.
В целом, я думаю, что причина того, что вы не видели формальных систем в «реальном мире», проистекает из того факта, что формальные системы доказательств уступили беспощадной тирании прагматизма. Как я уже упоминал, на создание ваших корректных доказательств уходит так много усилий, что это почти никогда не стоит. Промышленность давно решила, что создавать специальные тесты проще, чем проходить аналитические формальные рассуждения.