Поразмышлял письмом на тему спецификаций спецификаций [спецификаций спецификаций ...]

мета-мета-мета- ...

Сколь глубока это кроличья нора? Там же черепашки до самого низа? Ну, на самом деле да.

Открылась бездна, звезд полна,
Звездам числа нет, бездне дна.

Увы, но желаемая полнота в общем случае неразрешима (привет от Гёделя).

Бородатый пример -- система радиотерапии Therac-25, которая убивала пациентов. Код работал по спецификации, да только спецификация была неверной... А сколько сейчас такого вокруг нас, особенно с учётом вайбкодинга? да на каждом шагу.

Формализация мета-спецификаций кстати существует давно, это вопрос философский :) Это т.н. refinement calculus, но по ним на вики крохотная заметка с упоминанием пары работы с семидесятых и девяностых и всё.

При проектировании некомпьютерных КИИ (ядерная энергетика, авиация, оборона...) как правило применяется такой подход, когда несколько команд (две чаще всего, потому что сильно дорого) пишут свои независимые спецификации, которые затем сравниваются.

Вместо полной спецификации можно делать нечто property-based (инвариантность, монотонность, идемпотентность, коммутативность), и я кстати к этому фактически и пришёл, разбираясь с формализацией агентских оркестраций, в том смысле что свойства должны быть композируемы.

Но в любом случае каждую n-мета-спецификацию надо хотя бы минимально проверять на корректность через (n+1)-мета-спецификацию, и получаем тех самых черепашек, или фундаментальный предел формальной верификации -- проблема "specification gap". А на практике всё сводится в конечном итоге к человеческому намерению, которое неформально + недетерминировано + противоречиво + меняется со временем + у разных людей разное.

И вот тут AI может стать весьма хорошим мостом между естественным языком и формальной спецификацией. Чел описывает намерение словами, AI предлагает формальную спецификацию, человек верифицирует что она соответствует намерению... и мы попадаем в ту самую темку AI-DSL и заветы Алана Кэя, о чём я уже много раз писал. Это я уже по третьему ортогональному направлению тут разбираюсь, и каждый раз прихожу к одному и тому же :)

Мета-спецификации не решают проблему черепашек, но они её структурируют. Фишка не в том чтобы верифицировать всё "до самого низа", а в том, чтобы явно обозначить, где заканчивается формальное, и начинается человеческое. Точнее не где заканчивается, а где его оптимальнее всего закончить и, главное, как.

И это место - граница между намерением и формализацией - по сути Священный Грааль всей программной инженерии. И самое наименее изученное.

Ну ok, вызов принят, формальная философия ведь тоже наша любимая темка )