...И куда тогда дальше двигаться стратегически? Чтобы закладываться хотя бы на конец текущей десятилетки, когда AI станет генерить невероятные кучи дурно пахнущего кода, причём такой вайб станет по сути стандартом? Какие скиллы будут ключевыми?

...Где-то с осени 24-го я не читал ведущих спецов computer science, на днях заглянул в твиттер -- изменилось всё! Поголовный вайб-кодинг. Захлёбываясь от восторга, известные математики хвастаются, как ЖПТ им написал расчётный алгоритм на сто питонячьих строк.

Почему, как оказалось в итоге, я пояснял:
Математика существенно проще, чем программирование.

Так что же будет будущим программной разработки?

Тестирование. QA. TDD. BDD. TLA+. Формальные спецификации и математика уровня HoTT.

Программисты, по большому счёту, и сегодня пишут просто рандомное дерьмо, для которого ни до ни после не сформулированы никакие правила и ограничения.

Конечно, ЖПТ их вполне сможет заменить.

Специалисты по системному контролю качества, Гуру интеграционных тестов, Мастера формальных технических заданий -- именно это и будут те Инженеры, кто знает, как на самом деле должно работать всё это программистское 💩

Я решил пойти по пути Аяза Сэма Альтмана: добавил сегодня в ачивки карьерного трека темку "свой ИТ-бизнес" (своего рода генерик предыдущей "платный блог"). Пока необязательная, чисто по желанию; кто из моих курсантов по теме карьеры занимается на формате 2, с полного нуля помогаю пока БЕС-ПЛАТ-НО.

У Альтмана есть закрытый чатик с друзьями (вот ровно как у меня теперь), где они делают ставки на то, кто первым заработает 1 миллиард долларов в бизнесе одного человека (то есть вообще без помощников даже на рутину и оперативку). И так-то там уже немало пацанчиков и тянок, которые в одно лицо давно пробили отметку в 1 миллион, а в этом году уже и 10 миллионов долларов -- с помощью AI, соцсетей и цифровых продуктов (причём далеко не все там программисты).

Я наверное расширю мой список блогеров, где тоже будем делать аналогичные ставки :)

С чего начать? С мета-правила: не ссыте!

Из сегодняшних чатов:

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

Дорогие! В 2025-м вам надо не просто прокачивать блог и гитхаб.

Вы должны ВЫЁБЫВАТЬСЯ!!1

И это не метафора.

От одного из наших блогеров:

...Мой блог наконец приносит плоды, меня нашли не через блог, но я сразу козырнул им HR'ке, она передала его парням, СТО пришел уже под впечатлением, не выяснять мои компетенции, а подтверждать и знакомиться.
Да, я хорошо помню что называть первым число тактически может быть не верным, но я на $8k с радостью уйду :)

P.S. Дальше, напишу, какая самая прибыльная ниша для онлайн-бизнеса в 2026-м для программистов. Вписался для разминки вчера в пару платных блогов на сабстэке, ровно для вас.

...И первый шаг к миллиардерству - это конечно же глубоко освоить Arch Linux. Какой-то пакман-шмакман... как хорошо было на убунте :)

Каждый курсант теперь в обязательном порядке должен установить arch и поработать из него: это научит вас бесконечно большему знанию компьютеров, нежели любой онлайн-курс.

Сейчас я слушаю классическую музыку, работаю в Arch и чувствую себя натуральным психопатом.

p.s. ладно...

sudo pacman -S mc

...Но прежде чем стать долларовым миллиардэром, сперва надо быть не оштрафованным на рублёвые миллионэры )

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

Поэтому политика обработки перс.данных моей Школы такая: никакой политики!

Дорогие, у меня никогда вообще ничего вашего персонального не хранилось, не хранится и не будет; в майсикле зенона чисто ваши ники на учебном сервере и всё, даже логов и истории занятий не веду принципиально, а бэкап всей учебной базки за семь лет едва дорос до 500k, да и то там 70% sql-код. Минимализм a la arch - это наше всё.

(Но я на всякий случай добавил в базу галку "согласен на обработку ПД", кто не согласен немедленно уходите :)

=

То есть если например вы в экселе списочек клиентов локально ведёте,
или если вам отправляют ПД для заключения договора - вы оператор ПэДэ, потому что ваш ноут считается формально ЦОДом. (Я-то старая школа, в бумажной тетрадочке в клеточку, что не подпадает...). Если зарегили абтюя-кассу для приёма платежей онлайн, транзакции там -- это тоже ЦОД => собачьей рысью в РКН.

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

То есть вообще любой цифровой чих совершенно реально можно обозвать "оператором пэдэ". Чатик в тг с регистрацией -- явный сбор ПД. Личная страничка с фотками друзей -- ПД (ибо штрафы нехилые и для физлиц).

=

Бизнес в России развивать легко и просто, говорили они...

Причём высокие чины вам заявят что "это другое", а на практике низшие тупо штрафанут только так, и жаловаться пойдёшь в Спортлото.

Trae -- внезапно классная и лёгкая совсем AI-IDE, и стоит существенно дешевле этих ваших курсоров, и free режим неплохой. На скрине это я делаю в ней второй курс по гомотопической теории типов (хотя, по-прежнему, удобнее автономного ai-чатика нету пока ничего).

Риторическое: почему бы нашим не делать что-то подобное вместо монструозных и неповоротливых IDE наподобие GIGA-фигига...

🔥 5 причин, почему Carbon — это новый король системного кода! 🔥

Google's Carbon Language: An experimental successor to C++

1️⃣ 🚀 Память без головной боли
▸ В C++ утечки, use-after-free и UB — это как игра в русскую рулетку 💀.
▸ Carbon гарантирует memory safety на этапе компиляции — никаких ночных дебагов с valgrind!

2️⃣ 🔄 C++ совместимость без боли
▸ Rust требует переписывать всё с нуля ❌.
▸ Carbon работает с C++ напрямую — подключаешь старый код и постепенно мигрируешь.

3️⃣ ⚡️ Нулевые накладки, но с предсказуемостью
▸ C++: "Ой, а почему этот std::vector внезапно тормозит?" 🐢
▸ Carbon: Гарантированная производительность как у ручного C++, но без сюрпризов.

4️⃣ 🧩 Синтаксис для C++ девелоперов
▸ Rust с его ownership model — это как учить китайский 🈶.
▸ Carbon — почти как C++, но без кучи граблей. Переход за дни, а не месяцы!

5️⃣ 📈 Миграция без риска
▸ Chrome уже тестирует:
✔️ 0 багов с памятью
✔️ +40% к скорости код-ревью
▸ Можно начинать с малого — не нужно «всё или ничего».

💼 Вывод:
Carbon — это C++ 2.0 для тех, кто устал тушить пожары в продакшене. Если у тебя тонны legacy-кода, но хочется спать спокойно — это твой выбор. 🚀

P.S. Rust хорош для новых проектов, но Carbon — единственный путь для гигантов вроде Google. Держи курс на будущее! 🔮

AI сегодня приносит вашему боссу огромные сверхприбыли: вы станете делать тикеты в 2-8-32-128 раз быстрее, а ваша зп не вырастет при этом даже на 0,2% (ну вам же платят "за рабочие часы").

Поэтому, база: если есть хотя бы маленький выбор, НЕ используйте AI в найме (а только для своих проектов). Вырабатывайте спокойно рабочие часы, изучайте полезные темки гуглом и SO, прокачивайте свои реальные скиллы.

Но если будут прям настаивать, требуйте Курсор/Виндсерф/Трэй с корпоративным тарифом, и задействуйте его по максимуму прежде всего для самообразования (Агенты, MCP, ...), изучайте для себя, потому что ЖПТ это уже достаточно сложный отдельный скилл.

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

Если вы можете просто нормально разговаривать с людьми, вы опережаете 98% программистов.

- где учился?
- мгу
- чего мычишь? разговаривать-то умеешь?

Отчёт за неделю.

Последний набор в мою Школу для начинающих с полного нуля (3 места закончились за 28 минут)
Следующий набор будет осенью или в 2026-м. Но есть нюанс...
Раз в месяц (вот как сегодня) я открываю одно место на начальный курс-тест "Годитесь ли вы в программисты". Кто его успешно проходит может, продолжить в моей Школе. Но найти это место - хардкорный квест уровня хакерских паззлов из "Quadrilateral Cowboy".
p.s. Хм, кто-то быстро уже нашёл :)


Основной паблик:

До ЭПИЧЕСКОГО сбоя всех систем, работающих на Linux/Unix, осталось ВСЕГО 13 лет! Ну и?
Я в своё время поучаствовал, да и неплохо подзаработал, на проблеме Y2K, но 2038-й тогда казался чем-то вообще из другой Галактики...


Для донов-начинающих:

Мы оба знаем, что чтение (и тем более просмотр) любых учебных и образовательных материалов само по себе не изменит нашу жизнь. И вот что делает тебя несчастным ...


Для донов-неначинающих:

38. Жёсткий хейт SOLID | LSP (СильныеИдеи++)
Пояснение LSP в рамках SOLID весьма небрежно и расплывчато. Subtypes -- понятие достаточно строгое, но большинство разработчиков смешивают например подтипы с подклассами, после чего мы погружаемся в бесконечные разбирательства наследования на основе классов в духе is-a и has-a. Моделирование сущностей на таком уровне характерно примерно для 1980-х годов, когда мы пытались впихнуть круглое в квадратное под предлогом "ведёт-себя-как", "может-иногда-использоваться-как", "выдаёт-себя-за-того-на-кого-похож", с обязательным упоминанием утиной типизации...


Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но дружелюбные цены уже начали расти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small

=

Курс "Гомотопическая теория типов для программистов (2)" в процессе.
Реализовал группоиды (включая ∞ и высшие пути), n-мерные гомотопические группы, бесконечные последовательности гомоморфизмов, методы для вычисления гомотопических групп, усечения, стягиваемые типы...
Этим летом курс 💯 будет готов.

Продолжаю работу с курсантами 🤓

...Создал на hh новый аккаунт и сделал резюме аналогичное тому, что у меня, чтобы откликаться на все вакансии 300 т.р. и выше. Делаю отклики по 1-2 в день последнюю неделю. Всего пока около 10 откликов. Удивительно, но пока ни одного предложения даже на собеседование прийти не получил.

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

...прошел доп. курс о лямда-исчислениях за 12 минут.
Если честно, было сложно, я потратил часов 8 на это, вместо 12. И все еще не уверен, что все понял)
Довольно сложно в таких абстракциях думать, мозг, прям, напрягается.
Хотя, у меня в универе был хаскель 10 лет назад. И даже пролог)
Кажется, что тогда это давалось проще, может, мозг к работе адаптировался и другое, видеть не хочет))

Да, хаскель это по сути лямбда-исчисление и есть, но если это не понимать, то будет от хаскеля в основном только вред.

...Сам от себя в изумлении какие имена для персонажей и машин возникают в голове посреди ночи.
(это мы делаем с курсантом дипломный проект -- клон Стравы/Яндекс-такси - по моим меркам, сегодня чисто джуниорская темка)

...я сегодня очень удивился, изучая новую инфру своей команды и онромное количество микросервисов, наткнулся на proxy-сервис к бд и что я там увидел, а там все данные хранятся в формате JSON в PostgreSQL, прям как в последних задачах по SQL. Таким образом я получил от этого курса пользу буквально сразу же, конечено, у нас нет таких сложных запросов, как последние из 5 ваших задачек, но за то увидев миграции и данные я не теряюсь и могу спокойно с этим работать, отличный курс! Буду перерешивать задачки по мере изучения SQL на работе

...Вот буквально сегодня на работе столкнулся с подобной проблемой. Нужно было вывести некоторые метрики приложения из БД в графану. Но разработчик, который писал приложение, реализовал модель в БД таким образом, что просто так получить простую и понятную, элементарную информацию нет никакой возможности. Вместо простого подключению БД в качестве источника в Grafana и написания одного запроса нужно писать скрипт, который в цикле обращается к несокольким эндпоинтам API, выполняет преобразование полученных данных, записывает итоговые данные в отдельную БД с метриками. И уже из сторонней БД можно будет получить эти метрики. А можно было предусмотреть "информационную избыточность" и реализовать удобную модель данных для этих целей.

...В остальном существенно перестроил свой быт - ежедневно, после ужина, “выхожу во вторую смену” и засиживаюсь за решением, как правило, до часу ночи. Отказался от просмотра видосиков и пивка по вечерам. Отказываю в общении и мероприятиях в пользу программирования. Но чувствую, что на данном этапе такого усердия с моим уровнем всё-таки не достаточно.
Хочу поделиться радостью - спустя два месяца изучения азов программирования я написал свою первую рабочую программу на работе - мне необходимо было рассчитать количество ставок до момента достижения предельно допустимого лимита в аукционе. Любопытно, что у меня не возникло желания сделать расчёт по-старинке в excel - я сразу открыл python tutor и написал работающий код полностью по памяти!

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

Резюме такое, дорогие, что эйчары, а потом и AI, сломали ИТ-найм в России более чем полностью. Всё началось с того, что они стали фильтровать джуниоров по опыту, в ответ те начали крутить опыт, и в итоге всё предсказуемо закончилось тем, что сейчас на нормальную типовую вакансию 3-4 года опыта сразу прилетают сотни однотипных полуфейковых резюме, и в этом потоке вы потеряетесь просто статистически.

Впрочем, про важность нетворка я твержу последние лет пять, но за всё время из сотен ребят прокачал его от силы 1%, а полуживые блоги завели, может, 2-3%. Штош.
Вы никому не нужны, и никто вас жалеть не будет 👊

Ещё раз: найм в ИТ сломан, и никаких перспектив к восстановлению нету и не будет. Вообще независимо от вашего опыта и скиллов, работу шаблонными способами больше найти невозможно, только потратите кучу времени впустую.

Поэтому я вношу изменения в курс карьеры: дорогие, с лета 2025-го года для поиска работы от вас требуется не вылизанное резюме с сопроводительным письмом, и не упорство в бесконечном хомячьем тапанье по вакансиям, и не помощь ментора, и даже не софт-скиллы: от вас теперь требуются брутал-скиллы. Всё подобное остальное будет лишь их естественным следствием.

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

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

А уж "войти в айти с нуля" -- это реально задача уровня разведчиков-нелегалов ГРУ 😎

Этим летом, к осени, и будем это всё развивать 💪🏻

Тут ещё вопрос открытый, какую сторону выбрать :)
Тёмную понятно на порядки выгоднее, но и настолько же рискованнее.

В 2023 году токен TITAN (на базе ERC-20) потерял $2 млн из-за ошибки в кастомной функции transferFee. А моя верификация на 100 строк её уже сейчас ловит.

Lendf.Me (ERC-20) был взломан на $25 млн из-за reentrancy в обновлённой логике.

Сейчас активируются атаки ERC-20 "approve race",

и это только всего лишь ОДИН простейший крипто-протокол!

=

То есть, я потенциально уже могу запилить математически обоснованный SaaS, который будет
автоматически генерировать типы для основных компонентов контракта,
автоматически генерировать доказательства свойств контракта,
автоматически находить уязвимости,
автоматически генерировать тулзу для хака крипты и сливать в даркнет
и т.д.

И я уже, честно говоря, думаю, что зря сделал первый курс по HoTT со всеми исходниками открытым моим курсантам, и всего за 50 долларов.
Видите же, какую золотую жилу 💰 раскопал )
Пожалуй, повышу цену для начала в джва раза, и скидок никаких для этого трека не будет. И дальше цена будет только расти по мере того, как я буду эти изумрудные зёрна отыскивать по темке формальной верификации на базе хотт.

Хотя конечно ключевая фишка не в коде, а в методологии, а ещё точнее, в моей черепушке.

Можно запустить бобркоин для инвестирования в фейковый стартап такую пирамиду прорывную технологию.

Вопрос из мейнстрима: но почему всю эту верификацию не сделать просто обычными тестами?

Главное, что тестирование проверяет, что программа работает правильно на конкретных тестовых случаях.
Например, можно проверить, что Diffie-Hellman вычисляет общий ключ правильно для фиксированных g, p, a, b.

HoTT -- это доказательство. Оно гарантирует, что программа работает правильно во всех возможных сценариях .
Например, можно доказать, что общий ключ в Diffie-Hellman всегда совпадает, даже если злоумышленник перехватывает сообщения (через Path-типы и HomSpace).

=

Тестирование плохо справляется со структурными инвариантами (например, проверка, что вектор всегда имеет длину n).

Я же могу закодировать такие инварианты в типах:

vector = Pi(domain=int, codomain=lambda n: list, function=lambda n: [0] * n)

=

Тестирование требует ручного написания проверок для каждого случая.

HoTT позволяет использовать автоматические методы (например, SMT-солверы, Z3 с моего курса) для доказательства сложных свойств. Она позволяет моделировать атаки через Path-типы и проверять их невозможность.
Например, можно доказать, что злоумышленник не может создать ложный общий ключ, через Sigma-типы для доказательства корректности шагов протокола.

=

Тестирование работает с конкретными значениями , но не с криптографическими абстракциями . Например, нельзя проверить, что хэш-функция необратима.

HoTT позволяет моделировать криптографические примитивы через зависимые типы. Например, я могу определить тип EncryptedMessage, который гарантирует, что сообщение не может быть декодировано без ключа:

EncryptedMessage = Sigma(domain=str, codomain=lambda m: not is_decodable(m), first=message, second=True)

=

HoTT -- это выход на уровень формальных математических методов , где:
-- cвойства доказываются, а не проверяются;
-- структуры данных и их инварианты моделируются на уровне типов;
-- возможны автоматические доказательства и формальный анализ атак.

Конечно, подобные сервисы имеются, крипторынок ведь мультитриллионный. Дальше разберу несколько наиболее известных.

EasyCrypt -- теорем-прувер, фактически небольшой интерактивный фреймворк со своим языком, для формальной верификации криптографических протоколов, которые представляются в виде императивных программ. Большой плюс, что интегрируется с Coq.

It has four built-in logics:
- a probabilistic, relational Hoare logic (pRHL);
- a probabilistic Hoare logic (pHL);
- an ordinary (possibilistic) Hoare logic (HL);
- an ambient higher-order logic for proving general mathematical facts and connecting judgments in the other logics.

Какие минусы в сравнении с моим подходом:

-- В HoTT равенство -- это гомотопия (путь между типами), что позволяет легко и просто формализовать инвариантность и эквивалентность структур (хотим доказать, что два протокола (реализации) "эквивалентны" в смысле безопасности).
Например, в EasyCrypt доказательство того, что a+b=b+a для целых чисел, требует явного аксиоматического подхода. А в HoTT это следует из свойств абелевых групп (коммутативность встроена в структуру).


-- EasyCrypt требует явного моделирования условий безопасности (например, случайных оракулов или свойств конфиденциальности).

HoTT позволяет инкапсулировать эти условия в зависимые типы: можно определить тип SecureProtocol, который автоматически требует доказательства свойств безопасности.
Например, HomotopyGroup(Protocol, 1) ≡ 0 для первой гомотопической группы.


-- EasyCrypt работает с конкретными алгоритмами и их реализациями.

HoTT позволяет моделировать абстрактные математические структуры (группы, кольца, категории...), которые есть самая база криптографии, что упрощает доказательства теорем о безопасности, основанных на алгебраических свойствах.
Например, классы LoopSpace и HomotopyGroup могут быть использованы для анализа топологических свойств криптографических протоколов (устойчивость к циклическим атакам, ...).


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

=

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

И тут кстати большой вопрос, а насколько эти сервисы сами верифицированы в плане своей реализации? :) А если там программный баг, или ошибка в логике?

У меня по крайней мере логическая реализация HoTT проверяется тестами и стандартным чек-листом просто по "Homotopy Type Theory: Univalent Foundations of Mathematics". А возможно кстати, сделаю формальную верификацию и моей реализации, в качестве хорошего примера.

(Размышления письмом завтра продолжу, ещё парочку фреймворков разберу, чтобы как следует эту темку продумать)

Прувер Tamarin -- a security protocol verification tool that supports both falsification (attack finding) and unbounded verification (proving) in the symbolic model. Security protocols are specified as multiset rewriting systems and analyzed with respect to temporal first-order properties.

Это вообще сборная солянка самых разных формальных подходов, друг с другом практически не интегрирующихся.

Кусочки универсальной алгебры, символьные вычисления первого порядка, состояния моделируются через логические формулы (например, в SMT-солверах или в BDD), стандартный модел-чекинг, процесс-алгебры (π-исчисление, ...),.

+перезапись термов конечно - темка топчик, но я рассказывал:
"Компиляторы, автоматы, AST, правила вывода, разбор json, редьюсинг алгебраических выражений, паттерн матчинг и многое многое другое -- это всё про переписывание термов."
Для серьёзных задач требуются сотни гигов оперативки:)

Написан Тамарин кстати на хаскеле, и должен заметить, что сильная система типов при создании подобных фреймворков для работы с ещё более сильной системой типов -- это никакой не плюс, а минус. Я уже писал об этом , Lean (функциональный язык с завтипчиками) -- казалось бы почти готовая HoTT, смоделировать гомотопическую теорию будет легко и просто, но нет. Сильная система содержит уже по своему определению сильные ограничения, никуда из неё уже не рыпнешься.

"...Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции."

Казалось бы, ну что, я умнее академиков что-ли, что я это понимаю, а они нет?
Тут сермяга в том, что я смотрю на это с точки зрения опыта и программной инженерии,
а у них это просто классика фейлов стартаперства, любой миддл знает: взялись пилить проект, особенно если он сложный и наукоёмкий, а потенциальные архитектурные ограничения проявились, только когда половина бюджета освоена и поздняк метаться. И "правильно было бы переписать всё заново с нуля" :)
Cобственно выбор хаскеля 💯⛔️

Мой же инсайт, что лучше всего получается на питоне, а начинал я это делать вообще на php, и альфа-версия на сайте работает :)


— Tamarin ограничен моделью маркированных графовых автоматов LTS, сети Петри и т.п., где переходы между состояниями описываются одномерными правилами перезаписи. Сложные структуры (например, гомотопии) требуют ручной абстракции.
— HoTT через высшие индуктивные типы позволяет моделировать многоуровневые переходы и гомотопические пути между состояниями, что особенно полезно для проверки свойств с топологической природой (криптографические протоколы с нелинейными взаимодействиями...).

— В Tamarin инварианты, зависящие от значений, требуют явного программирования и дополнительных проверок логики.
HoTT через зависимые типы позволяет кодировать инварианты протокола непосредственно в типах.

— Tamarin использует автоматизированные методы (дедукцию...) и классическую логику и для сложных протоколов может вообще не завершить работу
HoTT основана на конструктивной логике, где доказательства представляют собой вычисления.

— В Tamarin для доказательства эквивалентности требуется явно моделировать обе версии протокола и сравнивать их поведение.
Унивалентность HoTT позволяет легко и просто доказывать эквивалентности между структурами (например, между двумя версиями протокола, если они изоморфны).

— Tamarin работает с формальной общей логикой (AC, ассоциативность, коммутативность), но не поддерживает абстракции высшего уровня.
HoTT позволяет напрямую моделировать сложные математические объекты (группы гомотопий, усечения типов...). Во многих протоколах используются алгебраические структуры (Diffie-Hellman, билинейные формы) или топологические свойства (многомерные состояния...).

Резюме:
Tamarin эффективен для автоматизации проверки стандартных протоколов.

Мой подход через моделирование HoTT на языке со слабой системой типов и динамической типизацией предлагает более универсальную и математически более богатую среду для верификации, особенно для сложных протоколов с высшими структурами и зависимыми инвариантами.

(потерпите, немного додумать осталось :)

Наконец, ProVerif: символьный подход к анализу протоколов, аналогично Tamarin, но с акцентом на автоматизированное рассуждение о криптографических свойствах. База -- типизированное расширение пи-исчисления с криптографией, язык моделирования параллельных процессов...
Криптографические примитивы (шифрование, хэширование, подписи) моделируются через функции и уравнения. Символьная модель криптографии Долева-Яо, клаузы Хорна (привет, Пролог), по сути абстрактные методы анализа, которые авторы сами придумали:)
Сложные структуры данных (например, вложенные списки или рекурсивные типы) требуют ручного моделирования.

=> ProVerif будет более практичным -- для автоматического анализа криптографических протоколов в символической модели.

В HoTT же например, можно определить тип "протокол с условиями на последовательность шагов", которые автоматически проверяются системой, и так можно верифицировать протоколы с жёсткими структурными ограничениями,

HoTT интегрирует категориальную логику и теорию гомотопий -- мощные математические инструменты для доказательства свойств безопасности, что особенно полезно для анализа протоколов с распределённой логикой или сложными взаимодействиями (можно например формализовать, что протокол удовлетворяет условию инъективной эквивалентности.)

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

=

Всё, с темкой разобрался, я красавчик :)
В заключение остаётся ещё подумать, какие сделать правильные выводы из этого всего.

Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.

В заключение сериала про инструменты формальной верификации.

Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на Lean или Isabelle, кстати и на F*, но их формальные теории как я рассказал ↑ ↑ ↑ сильно проигрывают HoTT (вообще, Воеводский абсолютный гений computer science), а их экосистемы, по достаточно очевидным причинам, или совсем хиленькие или откровенно отстойные.

А вот связка Python (суперинженерная экосистема, с мощной поддержкой и символьных вычислений, и солверов, и функциональщины, и машинлёнинга...)
+ HoTT просто как маленькая библиотечка, получается просто огонь 💥

Посмотрите, какая будет возня если используете Coq + Galline :)
"Формальная верификация смарт-контрактов во фреймворке ConCert"

Но я с этим связываться точно не буду 💯
потому что, ну кто там заказчики догадаться несложно.
Например SELinux верифицированное ядро делалось по заказу Агентства нацбезопасности США. Верификация кода, криптоалгоритмов из этой же серии. Всяческий ЦэБэ или ГазМяс от них тоже недалеко ушёл.

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

C другой стороны связываться с чистой криптой мне просто физически противно 🤮

Как вариант крипто-игры
By 2026, the market for blockchain gaming is anticipated to have grown to $70 billion, an exponential growth rate.
но там ведь тоже каждый второй -- это гэмблинг кал 💩

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

...

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

Придумал в процессе написания!!1 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.

Заключительный пост сериала будет про это.