>> Проще? То есть, по-вашему, описание целевой семантики — это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как — поделитесь секретом?
> Простой в данном случае является не описание семантики, а взаимосвязь отдельных систем.
> Где модуль (система), отвечающий за конкретную семантику, рассматривается как отдельный
> компонент.В том-то и дело, что когда мы начинаем говорить о корректности работы программы, то в полный рост встаёт проблема проверки связей между модулями. Полная корректность — это далеко не только «этот параметр не должен быть меньше десяти». Такие проблемы действительно ловятся на том же уровне анализа, что работают современные оптимизаторы кода. Но это ни разу не доказательство корректности программы. Возьмите молоко, солёные огурцы и селёдку — все высочайшего качества — и совместите их в своём желудке. Каждый отдельный продукт (модуль) сам по себе в порядке (верифицирован), но вместе получается сильно стрёмная смесь.
> Вы пока что к сожалению демонстрируете отсутствие системного мышления, когда у вас
> все детали перемешаны в кучу на одном уровне.
Вы хотите сказать, что мы говорим о разных вещах? Охотно верю. Правда, я понимаю, о чём вы говорите. А вы закопались на своих микрооптимизациях-микроверификациях. Которые НЕ выполнят поставленную изначально задачу (доказательство корректности программы).
> Хотя если говорить в общем, все сложные вещи состоят из простых. И
> если не удается сложное разложить на простое, то вообще о каком
> анализе может идти речь?
Вот вы и смешиваете разные уровни в один. Доказать корректность одного модуля ещё как-то можно (хотя уже тут зачастую приходится использовать либо специальные языки — про это я уже говорил, — либо NP-полные решения — тупой перебор всех возможных комбинаций входных параметров). Доказать корректность достаточно сложного проекта, который работает с непредсказуемой внешней средой, практически нереально. Этот тезис был озвучен в изначальном комментарии, этот тезис был озвучен и мной в ответе на него...
>> Гениально! (кстати, я говорил об этом тоже, не знаю, почему вы мне мои же мысли тыкаете) Вот только если бы вы ещё и думали... Во-первых, строить такой верификатор (писать синтаксические средства, библиотеки, организовывать нужным образом код и т.д.) вы на чём будете? На обычных синтаксических средствах?
> Вы не знаете, что такое self-hosting? (Вполне достаточно, чтобы на "другом" языке
> [C, asm и т.п.] было сделано емкое ядро, остальное - селфхостинг).
Во-первых, то, что вы называете, это не self-hosting. Self-hosting — это, например, у FreePascal, который полностью сам себя собирает.
Во-вторых, как видите, я знаю, о чём вы (хоть и путаясь в терминах) говорите. А вот вы, изначально считая себя умнее собеседника, даже не попытались понять, что же до вас пытаются донести. А донести пытаются то, что это, опять-таки, получается среда "сама в себе". Да, _сравнительно_ легко можно построить специальную среду, в которой доказательство корректности будет производится автоматически. Но если это будет единственное её достоинство, то с тем же успехом её могло бы не быть.
Возможно, при разработке такой среды будут сделаны какие-то ценные наработки, согласен. Но в целом это напоминает Plan9: звучит красиво, а использовать неудобно.
> Многие компиляторы являются таковыми. И здесь мы плавно возращаемся к тому, что
> технологии, используемые для оптимизации во многом идентичны таковым, используемым для
> верификации. Только целевая семантика разная (см выше). Просто большиству нужна только
> скорость и ничего более (см. ниже о большинстве).
Вы путаете верификацию сравнительно простых, компактных конструкций, и верификацию целых моделей. На уровне моделей возникают новые требования, новые спецификации, которые нельзя проверить на уровне модулей. Грубый пример: вот у вас есть два автомобильных колеса и ось. Сами по себе все они могут быть прекрасными. И колёса могут прекрасно стыковаться с осью (верификация на уровне модулей). Но если колёса окажутся разного диаметра, то автомобиль получится косым. Вот только теми способами верификации, про которые вы говорите, это проверить нельзя.
А проверить можно только заранее выстроив модель автомобиля, на каком-то понятном верификатору языке. И это — весьма трудоёмкая работа. Не факт, что вообще полностью решаемая.
> Вы просто плохо знаете предмет. И вам сильно мешают стереотипы.
Что порекомендуете?
>> Во-вторых, таким верификатором будет сложно заинтересовать людей, если надо будет переписывать программы на новом языке. Такой верификатор будет бесполезен, ибо прежде всего актуальна задача проверки _уже_имеющегося_ кода. На куче разных языков.
> Странно слышать такое от человека, который интересуется OpenBSD.
Почему???
> Вы считаете, что либо всем, либо никому?
Не обязательно. Но давайте я напомню, с чего начался наш с вами разговор?
"Хотя на самом деле "на данном этапе развития средств анализа", и даже еще гораздо раньше, существуют уже достаточно методов организации кода таким образом, чтобы было возможно доказывать его правильность с помощью автоматизированных средств доказательств и анализа."
Так вот, хотя методы организации кода существуют, но речь-то изначально шла о конкретике: стек IPSec в ядре OpenBSD. Вы как будто не заметили этого. Потому что из ваших слов, чтобы как-то связать их с исходной темой, я могу сделать только вывод, что опёнковский стек IPSec надо переписать, используя другие "методы организации кода", которые, помимо прочего, по вашему (вроде бы — различать анонимов у меня пока экстрасенсорных способностей не хватает) собственному признанию, включают "специальным образом организованный код, специальные библиотеки. И возможно даже специальные синтаксические средства". То есть фактически вы предлагаете переписать стек IPSec заново. Но какое отношение это будет иметь к верификации текущего стека?! То, что вы предлагаете, это НЕ обеспечение верификации имеющегося кода. Это требование написания НОВОГО кода. По новым правилам.
> Большинством людей вообще информационные технологии не востребованы, если тупо по головам
> считать.
Смотря что понимать под востребованностью... но это уже совсем оффтопик.
>> А то, о чём вы говорите, это сферический верификатор в вакууме.
> Разберитесь в вопросе и попрактикуйтесь, и он перестанет быть для вас сферическим,
> только и всего.
В чём мне следует, по-вашему, попрактиковаться?
>>> А вы продолжаете описывать техники верификации произвольного кода на произвольном языке.
>> Да, потому что они востребованы.
> Вы явно путаете факт востребованности и факт существования.
Не путаю. Это вы невнимательно следите за темой, выхватывая произвольные слова. Как быдлогопник, который посреди какой-нибудь слишком умной фразы выхватит слово "член" и начнёт над ним прикалываться. Даже если это часть фразы "член предложения".
>> Компьютеры, между прочим, до сих пор толком не научились математические теоремы доказывать.
>> Хотя в этом направлении работы ведутся намного дольше, чем над верификацией программ на обычных ЯП.
> Уже давным-давно научились. По крайней мере, все что охватывается первопорядковой логикой
> (а это вся "классическая" математика, за исключением самой логики или точнее,
> разных логик, где собственно и начинаются проблемы "селфхостинга"). Другое дело, что
> математика, которая раньше доказывалась "на бумаге", вообще говоря не была строго
> формальной. Сама математика используется _другая_ для строгих доказательств. См. интуиционизм
> и конструктивизм. Что уже говорить о языках программирования.
О, прогресс. Печально, что если не спровоцировать (каюсь, фраза про "толком не научились" была провокацией), вы ничего толком сказать не можете, отделываясь безосновательными утверждениями.
> У вас опять стереотипы и неверная информация.
> Есть огромное число людей, которые таким же образом, например, убеждены, что в
> UNIX-системах отсутствует графика. По крайней мере до широкого раскрута ширпотребных Linux-дистрибутивов
> так думало большинство, которое об этом что-то слышали. И опять же
> даже сейчас большинство даже о Линуксе ничего не знают.
Я, к сожалению, не учёный. И даже — признаюсь — не имею высшего образования, хотя некоторые в моём возрасте уже второе получают. Поэтому могу быть не в курсе последних достижений (хотя и стараюсь следить). А исхожу сугубо из практических соображений.
> А вы все "заинтересованность", "востребованость". Кому надо, те и заинтересованы. И этого
> вполне достаточно для общего прогресса.
Повторюсь, вы сами изначально перепутали решение одной конкретной задачи (верификация кода IPSec-стека OpenBSD) с другой (создание системы для написания кода, позволяющей писать автоматически или хотя бы автоматизированно доказываемые программы).
>> Вот-вот. Верификация для верификатора получается. А должно быть наоборот. С ваших слов, автомобиль едет для того, чтобы сжигать бензин, а не нефть перерабатывается в бензин для того, чтобы, сжигая его, ехал автомобиль.
> Еще раз, это называется self-hosting.
Нет, это называется "лошадь с телегой местами перепутали".
> А в аналогии с автомобилем вы путаете энергоноситель с механизмом. Тогда по-вашему
> получается, что компилятор, собирающий себя - это тоже автомобиль ради бензина?
Видимо, вы не поняли аналогию. Кто из нас после этого узко мыслит? :)
> И вообще, все кто пытаются рассуждать об информатике в материально-механических аналогиях,
> обычно так из "трех сосен" выйти и не могут.
Да что вы говорите...
>> Полностью согласен. Правда, смысла в этой пафосной фразе в данном случае нет никакого. :))
> Смысл в этой "пафосной фразе" такой, что вы далеко не первый, кому
> кажется, что он "все-все-все об этом знает".
Мне так не кажется. В отличие от вас.
Попробую резюмировать:
1. Изначальную задачу предлагаемые вами средства НЕ решают.
2. Тем не менее, они работоспособны.
3. Но насколько они подходят для решения реальных задач? Если такая автоматическая верификация будет требовать в 100 раз большие по размерам накладные расходы (как-то: вычислительные мощности, трудозатраты на описание модели, уменьшение производительности труда каждого отдельно взятого кодера и т.д.), то вопрос о практической ценности такого решения будет стоять весьма остро.
Автоматическая верификация, как любая технология, нужна не сама по себе, а для решения конкретных задач. В данном случае задачей является улучшение ПО. И если при решении данной задачи существенно ухудшатся другие параметры, то ещё не факт, что такая система будет нужна.
А ненужное отмирает. Закон жизни.
