(сегодня буду много постов размышлять текстом, важная тема, потерпите пожалуйста 🙏🙏🙏)

Сейчас тренд на всё своё "доморощенное" (в целом совершенно правильный, без иронии, я ещё с 90-х компьютерным журналистом в PC Week/RE написал сотни статей ровно о важности "национального" в ИТ, и свои взгляды никогда не менял, но тогда такие идеи были совершенно не в тренде). И вот наконец дождался, прошло всего-то 30 лет.

"свой ОС" "свой геймдев движок" "свой смартфон" "свой мессенджер" "свой проц" "свой приставка" "свой AI"...

Даже появилась "свой IDE" (где в about приведена ссылка на лицензию it-компании, которая демонстративно донатит врагам).

Хотя странно рассуждать о полноценном развитии "своего итэ", если оно не происходит прежде всего на базе своих фундаментальных разработок. Например, интел однажды слил полмиллиарда долларов из-за неверного проектирования чипа, и теперь активно применяет для этого всяческие системы верификации, включая SAT/SMT-солверы (формальные решатели). Как думаете, наши СБИС на каком софте проектируются, и насколько теперь ему можно доверять? А сегодня доля верификации в бюджетах таких проектов -- до 70% затрат на разработку СБИС.
Кстати, и рынок верификации смарт-контрактов с нынешних $300 млн. к 2030-му вырастет примерно в 7 раз, а у нас цифровой рубль, планируется крипту разрешить...

Но конечно никакого даже "свой солвер" нету и помине; в Стеклова и универах пользуют только зарубежные, вроде микрософтовского Z3 с кучей закладок для РФ.
Например, лекция микро-курс по SAT/SMT делал в МГУ приглашённый индус Vijay Ganesh. Хотя, по большому счёту, это уровень дипломного проекта, ну максимум аспирантского.

И уж тем более по формализации математики пустота. Филдсовский лауреат Tao вон буквально упарывается в обучении математиков современным it, и ключевой акцент, конечно, на proof assistant-ах и языках с завтипами: Coq, Lean, Agda, Isabelle, F*, Idris...

Coq ведь начинался усилиями советского математика Владимира Воеводского (гомотопическая теория типов), и посмотрите, что он сегодня представляет после ребрендинга: Rocq Prover. Вся академическая Европа и США сидит в основном на нём, и нам по определению на это теперь путь заказан.

Риторическое: надо ли делать "свой солвер", "свой пруф-ассистант", "свой формальный верификация"? При том, что последние топовые математики в этих темах уехали в европы...

Я кстати послезавтра Школу закрываю, серьёзно. Уже начались гонения штрафы онлайн-школ, кто без образовательной лицензии работает; принципиально не буду получать. В Индии например государство только поддерживает энтузиастов айти-обучения...