Читая тему [Зависимые типы] Объясните на пальцах.

Автор: BulatZiganshin
Дата: 03.07.09

я заметил, что существует некоторое недопонимание того, что такое баги, почему их стоит рассматривать так или иначе, и что дает верификация программ. Хотя, казалось бы, всё элементарно.

Итак, на вопрос, что такое баг распространен следующий ответ. Баг — это несоответствие программы спецификации. Существуют ли в реальном мире такие спецификации, которые формально описывают то, что делает программа? Очевидно, если же представить себе такую спецификацию, то она будет сопоставима по объему содержащей в себе информации с объемом самой программы. Между ними будет лишь то отличие, что программа будет содержать в себе некоторые детали реализации, относящиеся к взаимодействию программы с платформой, на которой она будет выполняться.
Спецификации такого размера никто, разумеется, писать никогда не будет. К тому же в самой спецификации могут содержаться ошибки.

Поэтому, я считаю данное определение слова баг полностью бесполезным. То есть "программа содержит баг" объективно не значит ничего.
Если посмотреть на большинство программ, содежащих баги (хотя это в некоторой степени зависит от предметной области), проблемы возникают не с тем, что программы выдают неправильный результат (работают не по спецификации), а в том, что они просто его не выдают. Вылетают с ошибкой Acsess Violation или, если язык поддерживает исключения, Unhandled Exception.

Поэтому стоит рассматривать баги, связанные с банальной корректностью программ с точки зрения вычислителя (ЭВМ) и среды (Операционной системы). Количество правил, которым должна удовлетворять программа в большинстве случаев фиксированно и известно.
В качестве примеров можно привести следующие Баги:
— некорректный (несоответствующий архитектуре) машинный код — неизвестная комманда процессора.
— недопустимое значение операндов — обращение по нулевому адресу, деление на ноль.
— нарушение целостности данных — запись данных за пределы выделенной памяти и повреждение кучи, попытка чтения данных за пределом буфера вследствие его неверного размера.
— необрабатываемые исключения
— зацикливание алгоритма
— несоответствие различных частей программ — не соблюдается договоренность (контракт) по области значений передаваемых данных.

На пути развития языков программирования с некоторыми багами научились бороться.
Изобретение языка ассемблера позволило писать код содрежащий только поддерживаемые процессором комманды. В общем случае это именно так, несмотря на то что всё равно существует способ подсунуть процессору черти что.
Изобретение Языка более высокого уровня (Си) позволило сокртаить количество багов, связанных с некорректными условными и безусловными переходами.
Языки с автоматическим управлением памяти и отсутствием указателей с арифметикой позволии избавиться от ошибок обращения по недопутимому адресу и порчи памяти.

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

Верификация программ направлена на значительное сокращение багов, путем проверки отсутствия определенных их классов без выполнения программы.
В современном понимании, я думаю, под ней в основном стоит понимать проверку на выполнение договоренностей (контрактов) по области значения данных.

Как раз для этого и было предложено использовать зависимые типы, поскольку описывая тип, можно наложить ограничения на значения данных (тип зависит от значения <=> установленно взаимооднозначное соответствие между типами и областями значений), которые будут иметь этот тип и тем самым перелодижить проблему соответствий областей значения данных на систему типов.

Интересно, почему в таком случае зависимые типы не пришли в мейнстрим (или пока не пришли), как это произошло, например, с автоматическим управлением памяти и сборкой мусора?

ИМХО существуют некоторые проблемы с реализацией языков программирования, поддерживающих зависимые типы, которые бы позволяли компилировать эффективный код. Например, возникает следующая проблема (я не знаю, решаема она или нет. Если да, то как?). Использование при программировании встроенных типов данных, хорошо поддерживаемых платформой (int, double, массивы). Насколько мы все знаем, в языках не поддреживающих массивы, имеются большие проблемы с производительностью (пример: хеш-таблица на хаскелле).
Как в том случае, если типы встроены в язык и их определение неизвестно, конструктивно описывать и доказывать их свойства?