> <...> Но давайте я напомню, с чего начался наш с вами разговор?
>
> "Хотя на самом деле "на данном этапе развития средств анализа", и даже еще гораздо раньше, существуют уже достаточно методов организации кода таким образом, чтобы было возможно доказывать его правильность с помощью автоматизированных средств доказательств и анализа."
>
> Так вот, хотя методы организации кода существуют, но речь-то изначально шла о конкретике: стек IPSec в ядре OpenBSD. Вы как будто не заметили этого.
>
>То есть фактически вы предлагаете переписать стек IPSec заново. Но какое отношение это будет иметь к верификации текущего стека?! То, что вы предлагаете, это НЕ обеспечение верификации имеющегося кода. Это требование написания НОВОГО кода. По новым правилам.
>
> Повторюсь, вы сами изначально перепутали решение одной конкретной задачи (верификация кода IPSec-стека OpenBSD) с другой (создание системы для написания кода, позволяющей писать автоматически или хотя бы автоматизированно доказываемые программы).

Нет, я ничего не перепутал, я именно об этом и говорил. И вы только что подтвердили, что вы прекрасно поняли, о чем я говорил. Ну разве что не обязательно переписывать, можно произвести рефакторинг. Для этого тоже есть автоматизированные средства. Какой ужас! По новым правилам! Да, для некоторых это страшный сон.

Это вы мне пытатесь навязать разговор о верификации стека.
Вам просто ваши стереотипы не позволяют "за деревьями увидеть леса". Верификация - это не "тема" и не цель. Верификация - это возможное средство, и при этом безнадежное. А цель и "тема" - сохранение заявленных качеств OpenBSD.

(Хотя конечно, если для вас "темой" является верификация стека - флаг вам в руки и успешного долбления головой "апстену".)

И поскольку я очень уважаю де Раадта, и те цели, которым он пытается следовать, я надеюсь, что он забил тревогу неспроста. Просто, как я надеюсь, он такими неординарными средствами с этим вбросом про бэкдоры пытается ткнуть носом в проблему таких стереотипных тугодумов, как вы.

> Вы путаете верификацию сравнительно простых, компактных конструкций, и верификацию целых моделей. На уровне моделей возникают новые требования, новые спецификации, которые нельзя проверить на уровне модулей. Грубый пример: вот у вас есть два автомобильных колеса и ось. .........

Почему нельзя? Может можно, да вы не знаете как.
Колеса и ось - это никакие не модули! Это физические объекты! Вы вообще не представляете себе что такое модули, раз такие аналогии приводите! (См. ниже)

Модель сложная? Ну так упростите! Анализ для чего нужен? Абстрагирование (как способность) зачем человеку дана?

> Вот вы и смешиваете разные уровни в один. Доказать корректность одного модуля ещё как-то можно (хотя уже тут зачастую приходится использовать либо специальные языки — про это я уже говорил, — либо NP-полные решения — тупой перебор всех возможных комбинаций входных параметров).

Здрасти! По вашему зачем вообще нужны модули? Разве не для упрощения? Т.е. у вас получается с модулями сложнее, чем без них?
Люди с недоразвитым системным мышлением придумывают какое угодно назначение модулей, но только не их истинное - упростить проектирование, анализ и эту самую верификацию.

Это наоборот обычно структура отдельных модулей бывает гораздо сложнее, и труднее поддается верификации, чем всясистема в целом. "Сверху вниз" бывает легче, чем "снизу вверх". Просто сразу видно, что вы проектировать не умеете. И у вас модули пещрят кучей взаимных связей, как у большинства "кодировщиков".

И кто вам говорил про необходимость NP-полных решений? Вы вообще представляете себе весь диапазон применения дедуктивных систем и прочего "ИИ"? Кроме "полных доказательств".

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

Трудоемко? Ай ай ай! Специальные языки, говорите, придется учить? А как вы хотели? Все на С? Ну нетривиально это точно. А вот степень трудоемкости зависит от умения проектировать и моделировать. По краней мере не так безнадежно, как верификация "традиционного" кода. Просто вы об этом ничего не знаете.

Еще раз, о "полной решаемости" вообще речь изначально нигде не шла. Все относительно. Это релятивистские системы, а не класические "абсолютные", как у вас с абсолютной "востребованностью". Однако как раз таки именно эта "трудоемкость" в достижении цели и снижается значительно.

> Компьютеры, между прочим, до сих пор толком не научились математические теоремы доказывать.
>
>> Уже давным-давно научились. По крайней мере, все что охватывается первопорядковой логикой (а это вся "классическая" математика, за исключением самой логики или точнее, разных логик, где собственно и начинаются проблемы "селфхостинга"). ...............
>>
> О, прогресс. Печально, что если не спровоцировать (каюсь, фраза про "толком не научились" была провокацией), вы ничего толком сказать не можете, отделываясь безосновательными утверждениями.

Ну уж конечно, это оказывается у вас была "провокация". В очередной раз дали ляпу, лишний раз подтвердив, что плохо разбираетесь в вопросе, а теперь вам стало стыдно, и вы пытаетесь оправдываться.

> Я, к сожалению, не учёный. И даже — признаюсь — не имею высшего образования, хотя некоторые в моём возрасте уже второе получают. Поэтому могу быть не в курсе последних достижений (хотя и стараюсь следить). А исхожу сугубо из практических соображений.

Ну так а чего спорите, если не в курсе? Ну так вы сначала докажите, что эти самые новые достижения непрактичны, вы же этого не доказали. Кроме того не такие уж они и новые, просто о них мало кто знает, и чтобы ими воспользоваться нужны дополнительные знания. Иначе ни задачи поставить не сможете, ни результаты не проинтерпретируете.

>> Во-первых, то, что вы называете, это не self-hosting. Self-hosting — это, например, у FreePascal, который полностью сам себя собирает.

Нет, это тоже селфхостинг, только не 100-процентный. Я лишь выдвинул критерий достаточности. Наличие емкого ядра, способного далее "вытянуть систему за шнурки". Если же удается добиться 100-процентного селфхостинга, то это еще "круче", никто не спорит.

Однако, я вижу вы поняли, зачем нужно, чтобы система могла верифицировать "саму себя" еще на начальных этапах. А если еще не поняли, то по крайней мере уже видите, что зачем-то такое делается даже во многих "традиционных" трансляторах.

> Вот-вот. Верификация для верификатора получается. А должно быть наоборот. С ваших слов, автомобиль едет для того, чтобы сжигать бензин, а не нефть перерабатывается в бензин для того, чтобы, сжигая его, ехал автомобиль.
>
>> Еще раз, это называется self-hosting.
>
> Нет, это называется "лошадь с телегой местами перепутали".

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

>> А в аналогии с автомобилем вы путаете энергоноситель с механизмом. Тогда по-вашему получается, что компилятор, собирающий себя - это тоже автомобиль ради бензина?
>
> Видимо, вы не поняли аналогию. Кто из нас после этого узко мыслит? :)

Ну да, конечно. Стоит вам лажануться, как оказывается, что либо у вас это была "провокация", либо вас не поняли.

> Во-вторых, как видите, я знаю, о чём вы (хоть и путаясь в терминах) говорите.

Да уж, оно видно, как вы "знаете".