Oleksandr Gavenko -> [email protected] @ 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.) -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
