Основывая на чём можно выбрать OCamL или Erlang или Haskell

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

Это расхожее клише. Программное обеспечение слишком ненадёжное, основные автоматические контуры защит тепловых станций делают механическими.

Для первого типа система типов хаскиля сильно недостаточна (тут зависимые типы, CoC и доказательства корректности)

Сильная система типов и статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише. Ариан-5 вполне себе успешно взорвалась из-за переполнения.

Сильная система типов и статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише. Ариан-5 вполне себе успешно взорвалась из-за переполнения.

Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

Кстати, в Ариан софт был на Аде, что символично: мертворожденный бастард языка-зомби Алгол был обречен на «успех».

Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

А я вот помню, как darcs с segmentation fault валился. Из-за ошибки в рантайме, написанно на Си, правда, но факт есть факт: формально нельзя доказать, что программа без ошибок работать будет.

> Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

Угу, но вот только:

1. Переполнений может и не будет, но будет какая-то другая херня, отсутствие которой ты _забыл доказать_. И нет никакого способа проверить - а доказал ли ты отсутствие всех классов багов или какой-то класс в каком-то месте оказался доказательством не покрыт.

2. Нет способа проверить правильность твоего доказательства. Это задача алгоритмически неразрешимая. Ты, конечно, можешь попытаться доказать, что доказательство верно. Но кто докажет, что верно это твое последнее доказательство? Никто. Т.о. наличие доказательства отсутствия ошибок не гарантирует, собственно, 100% отсутствия ошибок.

3. Нельзя доказать, что «программа работает», т.к. это понятие нельзя формально выразить. Можно доказать, что работа программы соответствует спецификации, но кто тебе гарантирует, что спецификация корректна (те самые «в спецификации забыли указать, что переполнений быть не должно» - как раз близки к этой теме) или хотя бы непротиворечива? Ответ: никто и никогда, это невозможно.

4. Реальная программа работает в реальном мире на реальном железе, спецификации которых во втором случае возможно, а в первом - обязательно - неполны и некорректны.

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

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

> статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише.

...придуманное противниками статической типизации %)