Re: сертификация
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Wed, 28 Apr 2010 10:55:18 +0300:
>> OG> Я бы сказал так - на Си код тяжело верифицировать,
>> OG> скорее всего придется отказаться от существующего кода
>> OG> и писать на более формальном языке - например Лиспе.
>>
>> У меня фортунка на эту тему любимая есть...
>>
>> Greenspun's Tenth Rule of Programming: any sufficiently complicated C
>> or Fortran program contains an ad hoc informally-specified bug-ridden
>> slow implementation of half of Common Lisp.
>> -- Phil Greenspun
>> "Including Common Lisp."
>> -- Robert Morris
>>
OG> OK!
>> Реализацию лиспа, на которой оно выполняется, кто доказывать будет?
>> -Пушкин- МакКарти?
OG> Было бы время и возможности.
Пара лишних возрастов Вселенной?
Реализацию CL на C доказать - это не баран чихнул. Даром, что ли,
безглючных не существует?
Вот Scheme еще можно пробовать.
>> И в общем, да, ты тот лисп вообще видел? Программы на нем писал?
OG> не CL но elisp достаточно, но это не важно
>> Отлаживал? А реальные программы, не учебные задачи? Я б тебя еще
>> понял, если б ты Хаскель назвал - тот чисто функциональный, там
>> действительно существенно легче верифицировать. А как только у тебя
>> в языке есть присваивание - все, туши свет...
>>
OG> в этой области профан
Ну, стало быть, и в доказательстве программ тоже профан.
>> >> OG> Доказательство же позволит избежать полного невозможного
>> >> OG> перебора для тестирования.
>> >>
>> >> Нивапрос. Если его удастся, во-первых, построить, а во-вторых,
>> >> проверить.
>> OG> Построить действительно на данный момент тяжело.
>> OG> Проверка же выполняется просто -
>> OG> убедаемся в правильности формализации
>> OG> и коректности правил вывода.
>>
>> "Ты пальцем покажи". В смысле - предъяви доказательство правильности
>> формализации любого _практического_ программно-аппаратного комплекса.
>>
OG> http://ertos.nicta.com.au/research/sel4/
OG> Информация разбросана по инету.
0. Это только программный. Я просил программно-аппаратный.
1. И практический.
>> OG> Доказательство проверится автоматичеки.
>>
>> Автоматическую проверялку доказательства уже доказали? А автомат, на
>> котором оно проверяет?
>>
OG> Было бы время и возможности.
... еще пара возрастов Вселенной...
OG> Но сложности все таки есть. Например
OG> http://en.wikipedia.org/wiki/Kepler_conjecture
OG> из осторожности не признают доказанной. Хотя машинное доказательство
OG> http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer
OG> было принято общественностью.
... т.е. общественность после продолжительных дебатов решила "черт с
вами, поверим".
>> >> Тесты ту же вероятность обычно дают дешевле.
>> >>
>> OG> В доказательстве нет места вероятности.
>>
>> Это очень наивное утверждение. Мягко говоря, не соответствующее действительности.
OG> Из wikipedia:
OG> In 2005 Benjamin Werner and Georges Gonthier formalized a proof of the four
OG> color theorem inside the Coq proof assistant. This removed the need to trust
OG> the various computer programs used to verify particular cases; it is only
OG> necessary to *trust* the Coq kernel.
OG> Вероятности *нет*.
Ну что значит "нет"? "Поленились оценить" - да, верю.
>> OG> Тесты могут обнаружить ошибку,
>> OG> но не могут гарантировать их отсутствие,
>> OG> тогда как доказательство гарантирует.
>>
>> Упущено ключевое слово. _Верное_ доказательство. И вот в этом слове и
>> прячется вероятность.
>>
OG> http://en.wikipedia.org/wiki/Computer-assisted_proof
OG> http://en.wikipedia.org/wiki/Interactive_theorem_proving
OG> http://en.wikipedia.org/wiki/Automated_proof_checking
OG> Ошибки в реализации конечно возможны, но замечу
OG> что доказательства прогонялись на различных версиях
OG> и для некоторых сложных мат. теорем имеются доказательства
OG> в различных системах.
"На различных версиях" - это вообще не аргумент. Различные версии имеют
тенденцию иметь близкие наборы ошибок.
Различные системы - уже лучше, но тоже, в общем... Понимаешь, фраза
"имеются доказательства в различных системах" - это тест, а тесты
могут... далее см. цитату из тебя же 20 строками выше.
OG> Было бы время и возможности для проверки правильности реализации
OG> proof checker'а.
OG> Я верю что спустя некоторое время общественность примет машинные
OG> доказательства как равносильные бумажным.
Я могу поверить, что компьютерное доказательство современной теоремы
более надежно, чем человеческое. Но вероятность того, что оно верно,
все равно отлична от 1. А вероятность того, что правильная программа в
реальной жизни однажды не сработает, даже вполне заметно отлична от 1 -
практика показывает, что даже для не шибко распространенного софта раз
лет в 10 такое всплывает.
Не говоря уже о том, что событие с вероятностью 1, как нас учит теория
вероятностей, тоже может не произойти как нефиг делать. (Мой любимый
пример на эту тему - выбор точки на отрезке [0;1]. Какая-то точка
обязательно будет выбрана - но вероятность ее выбора в точности равна
0.)
Reply to: