Зависимые типы могут подтвердить, что ваш код соответствует спецификации. Но как вы доказываете правильность спецификации?

Ответ 1

Это статическая версия системы типа Как вы скажете, что ваши тесты верны?

Единственный ответ, который я могу честно сказать, - это более сложная и громоздкая ваша спецификация, тем более вероятно, что вы допустили ошибку. Вы можете ошибаться в написании чего-то в формальном формализме типа так же хорошо, как вы можете в формализации описания вашей программы как исполняемой функции.

Надеемся, что ваша спецификация проста и достаточно мала, чтобы судить по экзамену, в то время как ваша реализация может быть намного больше. Это помогает в том, что, как только у вас есть формализованные идеи "семян", вы можете показать, что идеи, полученные из них, верны. С этой точки зрения, чем более легко вы можете механически и доказуемо получить часть своей спецификации из более простых частей и в конечном итоге извлечь свою реализацию из своей спецификации, тем более вероятно, что вы должны получить правильную реализацию.

Но может быть неясно, как формализовать что-то, что может привести к ошибке при переводе ваших идей в формализм - вы можете думать, что вы доказали одно, когда на самом деле вы доказали другое - или вы можете найти себе исследование теории типов, чтобы формализовать идею.

Ответ 2

Это проблема любого языка спецификации (даже английского), а не только зависимых типов. Ваш собственный пост - хороший пример: он содержит неофициальную спецификацию "функции сортировки", которая требует, чтобы результат был отсортирован, а это не то, что вы хотите (\xs -> [] будет квалифицироваться). См. этот пост из блога Twan van Laarhoven.

Ответ 3

Я думаю, что все наоборот: хорошо типизированная программа не может показаться бессмысленной (если предположить, что система является постоянной), тогда как спецификации могут быть непоследовательными или просто глупыми. Так что это не "как убедиться, что этот фрагмент кода отражает мои платонические идеи?", А скорее "как убедить мои идеи в значительном прогрессе в обоснованном плане чистых синтаксических правил?". Как убедиться, что птица, которую вы видите, - это пересмешник [для какого-то поставленного понятия насмешки)? Ну, изучайте птиц и повышайте шансы быть правыми. Но поскольку всегда с людьми, вы не можете быть уверенным на 100%.

Теория типов - это способ смягчения несовершенства человеческого разума путем введения формальных правил, проверенных машиной доказательств (это очень актуальная статья) и других материалов, которые позволяет сосредоточиться и, таким образом, упростить проблемы (как сказал Браувер: "Математика - это не более, не что иное, чем точная часть нашего мышления" ), но вы не можете ожидать, что какой-либо инструмент сделает ваши мысли "правильными", потому что нет единого представления о правильности. IOW, нет никакого способа формально соединить неофициальные и формальные: быть неформальным, как быть внутри монады IO - нет выхода.

Итак, это не означает, что этот синтаксис отражает мою очень точную семантику? ", а скорее" могу ли я присоединить свою сырую семантику к этому сильно структурированному синтаксису? ". Программы - это правильные материальные объекты, а идеи - громоздкие аппроксимации, которые могут стать подходящими материальными объектами только по соглашению. Таким образом, мы формируем некоторый базис, используя условные обозначения, и тогда мы просто доверяем ему, потому что гораздо разумнее доверять маленькому подмножеству всех ваших многочисленных идей, чем всем им.

Ответ 4

Как вы доказываете правильность математики? То есть, как вы доказываете, что целочисленное добавление является правильным способом подсчета яблок, или как вы доказываете, что реальное дополнение является правильным способом добавления весов? Существует всегда интерфейс между формальным/математическим и неформальным/реальным. Это требует умения и математического/физического вкуса, чтобы найти подходящий формализм для решения конкретной проблемы. Формальные методы не исключают этого.

Значение формальных методов двоякое:

• Вы не узнаете, правильная ли ваша программа, если вы не знаете, какие свойства она действительно удовлетворяет. Прежде чем вы узнаете, правильна ли ваша процедура сортировки, сначала вам нужно знать, что она на самом деле делает. Любая процедура для выяснения этого вопроса будет формальным методом (даже модульное тестирование!), Поэтому люди, которые отвергают "формальные методы", на самом деле просто ограничивают себя крошечным подмножеством доступных методов.

• Даже когда вы знаете, как узнать, что на самом деле делает программа, люди ошибаются в своих математических рассуждениях (мы не рациональные существа, какими бы ни были определенные идеологии); поэтому полезно, чтобы машина проверила нас. Это та же самая причина, по которой мы используем единичные тесты. Приятно проводить проверку стола и следить за тем, чтобы программа выполняла то, что мы хотим; но при этом компьютер выполняет проверку и сообщает нам, правильно ли результат помогает предотвратить ошибки. Предоставление компьютерам подтверждения наших доказательств о поведении программы полезно по той же причине.

Ответ 5

Одно из формальных методов может сделать то, что я не думаю, что другие затронуты, это помощь, которая связывает простые вещи с более сложными. Вы можете не знать точно, как точно указать, как должна выглядеть структура данных Set, но если вы можете написать простую версию на основе отсортированных списков, вы можете доказать, что ваша причудливая версия, основанная на сбалансированных деревьях поиска, через функцию toList. То есть вы можете использовать формальные методы для передачи вашей уверенности в сортированных списках в сбалансированные деревья поиска.

Ответ 6

Предположим, что ваша функция не является верхним уровнем, но используется кем-то еще как часть некоторого модуля, который также имеет доказательство правильности. Последний должен использовать подтверждение корректности вашей функции, а если это плохо, модуль не будет компилироваться. Сам модуль по-прежнему может иметь ошибки, но он больше не является проблемой для вас.

Ответ 7

Поздняя вечеринка, но AFAICT, никто еще не упомянул еще один важный аспект: в контексте проверки программы наличие ошибки в спецификации не всегда слишком ужасно, потому что вы можете использовать код для проверки спецификации.

IOW, в доказательстве не говорится, что "код прав", но "код и спецификация взаимно согласованы". Итак, чтобы ошибка в спецификации не замедлилась, она должна быть одной из следующих:

• неопределенная спецификация.
• ошибка в спецификации, соответствующая соответствующей ошибке в коде.

Как заметил кто-то другой: проблема одинакова для тестов.