OberonCore

Попалась в руки ссылка: http://elementy.ru/trefil/21142


Если перенести это на программирование, то можно ли сказать — разработчик софта занимается формированием системы аксиом, выраженной в исходных текстах программ? Мне кажется, это очевидно.

А вот теорема Гёделя ясно нам говорит — как бы ты не парился, проектируючи архитектуру, вылизываючи и рефакторя исходные тексты, твоя программная система никогда не будет идеальной. И в силу обязательного наличия неразрешённых предположений, где-то обязательно вылезут огрехи, потребующие всяческих вмешательств в виде, например, отладки.

Такое умозрение наводит на мысль, что пресловутая "читабельность" кода, всяческие утиные типизации и прочие пейтоны с хаскеллями суть жалкие попытки усилить ся немощного, дабы достичь недостижимого — а именно, полностью доказанной системы аксиом.

Теоремы Гёделя имеют очень конкретный, точный смысл, понятный математикам-теоретикам.
Не думаю, что стоит их так вольно трактовать.

Понятно, что возможности формализации и формального доказательства имеют ограничения.
Но проверка правильности - это не чисто формальный процесс.
Нельзя построить формальную систему, которая проверит завершимость цикла.
Но человек легко это проверяет.

Да и как-то сравнение пейтонов с хаскелями очень странное. При чём тут хаскель и утиная типизация? Утиная типизация и какая-либо доказательность (доказательность - это обязательно какое-нибудь статическое средство, а утиная типизация - принципиальный отказ от статики)?

Илья Евгеньевич. Следите за.

В смысле?

Можно перефразировать:
нельзя создать формальную систему (алгоритм), которая даст ответ о произвольном цикле, завершим он или нет, но человек даёт такой ответ.

Мне кажется, что теоремы о неполноте играют рояль в контексте доказательства правильности. Можно доказать правильность программы, но!... Это не означает, что правильная программа СООТВЕТСТВУЕТ техническому заданию (требуются дополнительные аксиомы... )

Гугл отсылает к некоему Успенскому, который не столь строг в интерпретации теоремы, и даже применяет её к теории алгоритмов (насколько я успел понять).
А если уж даже он неправ, то Гёдель может дальше оставаться строгим - копирайты же на теоремы не распространяются?

Ну, разве что: "мамой клянусь, завершим".

Имеем случай так называемого вранья.

Сравнения нету, потому что наверняка есть нужда в удобстве построения системы непротиворечивых утверждений, отсюда и любовь к "читабельности", краткой записи, динамической типизации и прочим ухищрениям. Мне кажется, что теоремы Гёделя имеют гораздо более глубокий (широкий) смысл, чем кажется многим математикам. И так кажется не только мне: http://awas1952.livejournal.com/824361.html

Драсте. А как мы доказываем, когда циклы пишем? Что вектор переменных сойдётся к условию цикла.
Понятное дело, что если цикл запутанный, то это трудно, но можно и "распутать" - и показать, что либо он правилен, либо нет.

Ну, Иван, Вы бы эта... не переоценивали. Любовь к выпендрёжу, лень, презрение к дисциплине у них - и причём тут Гёдель?
Автор Питона писал:

Короче, там принцип один "чо тут думать, прыгать надо, банан вот он".


[/quote]
Дык я не спорю. Только расширять смыслы нужно осторожно...

Возможно, что создатель Питона нашёл быстрый и приматичный способ формулирования аксиом

А мы пишем такие циклы, про которые можем что-то доказать.

В каковом выборе как раз и заключена высокая роль человеческого интеллекта.

Ну, пусть будет дан какой-либо немыслимый цикл с break-ами - его можно постепенно распутать и преобразовать в эквивалентный, в котором уже либо найдётся ошибка, либо окажется, что он всё-таки правилен. Кажется, что можно?

Креститца, креститца и ишшо раз креститца!

Некий Успенский - это вот этот. Правда, про Гёделя в основном в самой "Апологии математики" (статье). Вы имеете в виду, что если мы формализовали ТЗ, скажем, для проверки моделей - то это только при некоторых ограничениях (текстуально конечные типы)?
Ежели эти ограничения выполняются и в моделируемой системе (данные-код-аппаратура), то формальная верификация, видимо, заменяет отладку. Но требует формулировать все требования к системе. Что, вероятно, не всегда возможно сразу. Кстати, здесь многое связано не с Гёделем, а с алгоритмической разрешимостью (в частности, насчёт завершения цикла - и вообще алгоритма на конкретных исхданных). Хотя эти вещи, возможно, глубинно пересекаются как-то...
У Фридланда, кстати, интересный обзор - там, где про формализацию и алгоритмизацию. О том, что информатическое решение (представляемое через алгоритм) не всегда возможно при исходной постановке задачи, тоже...

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


http://ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте

Вы имеете в виду отладку ПО "методом эксплуатации" ?

Изничтожение break-ов это и есть уход в более сильную теорию.

Непротиворечивость какого-то конкретного цикла с break-ами будет доказана не в рамках теории "циклов с break-ами", а (прямо как Гёдель прописал) в рамках более сильной теории каких-нибудь там дейкстровских циклов.

Что касается самой "теории дейкстровских циклов", то она, видимо, в гёделевском смысле не полна.