Re: сертификация
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Wed, 28 Apr 2010 14:58:19 +0300:
>> OG> Я верю что спустя некоторое время общественность примет машинные
>> OG> доказательства как равносильные бумажным.
>>
>> Я могу поверить, что компьютерное доказательство современной теоремы
>> более надежно, чем человеческое. Но вероятность того, что оно верно,
>> все равно отлична от 1. А вероятность того, что правильная программа в
>> реальной жизни однажды не сработает, даже вполне заметно отлична от 1 -
>> практика показывает, что даже для не шибко распространенного софта раз
>> лет в 10 такое всплывает.
>>
OG> Дома стоят, самолеты летают.
Хороший пример. И дома, и особенно самолеты падают, прямо скажем, нередко.
OG> В софте есть проблемы - пишут его на коленках
OG> с использованием опасных языков програмирования
OG> для небезопасных платформ.
В том случае, который был у нашей конторы, ничем кроме взглюка железа,
объяснить проблему не удалось. С перепроверками этого места и попытками
воспроизвести проблему возились около года.
Кстати, известный факт - да, вероятность детерминированного выполнения
детерминированного алгоритма на существующем железе меньше 1. В
достаточной степени меньше, чтобы это вызывало вполне реальные проблемы.
И чтобы десяток прогонов вероятностного теста на простоту давал лучшую
вероятность того, что число простое, чем вероятность, что все
арифметические действия в процессе выполнились правильно...
>> Не говоря уже о том, что событие с вероятностью 1, как нас учит теория
>> вероятностей, тоже может не произойти как нефиг делать. (Мой любимый
>> пример на эту тему - выбор точки на отрезке [0;1]. Какая-то точка
>> обязательно будет выбрана - но вероятность ее выбора в точности равна
>> 0.)
>>
OG> Ага, мера Лебега одноэлементного множества
OG> на действительной прямой равна 0.
OG> В формальной логике нет понятия вероятности,
OG> либо имеется доказательство теоремы из соответствующих аксиом
OG> и правил вывода либо нет.
OG> Имеется эффективная процедура для установления того факта
OG> является ли последовательность утверждений выводом в логическом
OG> исчислении. А иначе как?
OG> Человеческий фактор есть проблема.
Причем в данном случае принципиально неустранимая. Можно только
уменьшить его влияние.
Reply to: