Очередное пророчество про конец программирования, и кстати достаточно серьёзное, как бы странно не выглядело.
"The Final Form of Software Development" (впн)

Разработка как минимум критических информационных инфраструктур, где требуется формальная верификация кода, сведётся к связке ассемблер + пруф-ассистант вроде Lean, потому что семантика ассемблера примитивная, только память и регистры. Автор пишет, что с помощью агентов с телефона каждый день делает полтыщи коммитов верифицированного кода ))) Причём агенты в своих доказательствах быстро находят неточности и сами правят. А рассуждать нейронке удобнее именно на формальном уровне, в формальной семантике, по этой теме поясняю в Функциональных архитектурах.

Сишечка не подходит потому, что подавляющий объём верификации тратится на доказательства отсутствия undefined behavior, ну а для rust семантику вообще определить невозможно, потому что она задаётся компилятором. Соответственно для КИИ требуется, чтобы и сам компилятор и рантайм были верифицированы, что создаёт с подобными прокладками огромные сложности. А с ассемблером действительно всё тривиально, компилятор простейший, рантайма нету.

Итог такой, полагает автор, что все языки, компиляторы и абстракции будут в конечном счёте переведены в эту ассемблерную парадигму, поэтому она конечна и в категорном, и в историческом смысле.

Ну хз :) Я бы помечтал, что например если формализовать все системы типов, System F, MLTT, HoTT, HOTT и др. (что уже кстати активно ведётся) и сделать для них единую синтетическую теорию-"крышу", то мы получим наоборот суперязык программирования, код которого будет верифицированным по определению, так как и спецификации можно записывать на нём же (откуда мы впрочем попадаем в темку спецификаций спецификаций, но это уже совсем другая история:).

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

ps. извините дорогие, у меня стоит защита от ботов, в час до 5 человек только пропускает, мне подписчики особо не нужны )