> -- Пётр Кушнир писал(а):
> Гугл отсылает к некоему Успенскому, который не столь строг в интерпретации теоремы, и даже применяет её к теории алгоритмов (насколько я успел понять).А если уж даже он неправ, то Гёдель может дальше оставаться строгим - копирайты же на теоремы не распространяются?Некий Успенский - этовот этот.Правда, про Гёделя в основном в самой "Апологии математики" (статье).> -- Валерий Лаптев в viewtopic.php?p=65963#p65963 писал(а):
> Мне кажется, что теоремы о неполноте играют рояль в контексте доказательства правильности. Можно доказать правильность программы, но!... Это не означает, что правильная программа СООТВЕТСТВУЕТ техническому заданию (требуются дополнительные аксиомы...  )Вы имеете в виду, что если мы формализовали ТЗ, скажем, дляпроверки моделей- то это только при некоторых ограничениях (текстуально конечные типы)?
Ежели эти ограничения выполняются и в моделируемой системе (данные-код-аппаратура), то формальная верификация, видимо, заменяет отладку. Но требует формулировать все требования к системе. Что, вероятно, не всегда возможно сразу.Кстати, здесь многое связано не с Гёделем, а с алгоритмической разрешимостью (в частности, насчёт завершения цикла - и вообще алгоритма на конкретных исхданных). Хотя эти вещи, возможно, глубинно пересекаются как-то...
УФридланда, кстати, интересный обзор - там, где про формализацию и алгоритмизацию. О том, что информатическое решение (представляемое через алгоритм) не всегда возможно при исходной постановке задачи, тоже...