Лаборатория Математики и Программирования Сергея Бобровского – Telegram
Лаборатория Математики и Программирования Сергея Бобровского
1.29K subscribers
1.19K photos
24 videos
930 links
ЛаМПовое с Бобровским
Download Telegram
🔥 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. Держи курс на будущее! 🔮
👍5111❤‍🔥3🤔2💯1
AI сегодня приносит вашему боссу огромные сверхприбыли: вы станете делать тикеты в 2-8-32-128 раз быстрее, а ваша зп не вырастет при этом даже на 0,2% (ну вам же платят "за рабочие часы").

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

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

А если начальники просто тупо мямлят что-то в духе "ой, ребятки, а давймте жэпэт чятики используен", ну ок, фигачьте по максимуму вайб-кодинг, который через несколько месяцев техдолг увеличит на порядок, и вы станете абсолютно незаменимым кадром и получите мощнейший рычаг давла :)
46💯13🐳8😁3👍2
Если вы можете просто нормально разговаривать с людьми, вы опережаете 98% программистов.

- где учился?
- мгу
- чего мычишь? разговаривать-то умеешь?
👍40😁22🤔4💯2🫡1
Отчёт за неделю.

Последний набор в мою Школу для начинающих с полного нуля (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-мерные гомотопические группы, бесконечные последовательности гомоморфизмов, методы для вычисления гомотопических групп, усечения, стягиваемые типы...
Этим летом курс 💯 будет готов.
👍344👌3🫡1
This media is not supported in your browser
VIEW IN TELEGRAM
Продолжаю работу с курсантами 🤓

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

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

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

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

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

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

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

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

...Вы нисколько не обманули, когда написали про задания ужасающей сложности, именно такими они и показались. Хотя по времени вышло не очень много, у меня это заняло 17 часов, но это были самые неприятные часы. Перед началом каждого занятия ещё требовалась моральная подготовка. Никому не могу порекомендовать этот курс и сочувствую тем, у кого есть подобное на проектах.
(Ну так-то такое на сегодня считается типичный миддловский бэк)
👍397🤯5💯5❤‍🔥1
Резюме такое, дорогие, что эйчары, а потом и AI, сломали ИТ-найм в России более чем полностью. Всё началось с того, что они стали фильтровать джуниоров по опыту, в ответ те начали крутить опыт, и в итоге всё предсказуемо закончилось тем, что сейчас на нормальную типовую вакансию 3-4 года опыта сразу прилетают сотни однотипных полуфейковых резюме, и в этом потоке вы потеряетесь просто статистически.

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

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

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

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

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

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

Этим летом, к осени, и будем это всё развивать 💪🏻
43👍19😁7❤‍🔥5💯4
...Первый шаг к долларовому миллиардерству -- выбор ниши для "цифрового продукта". Ну, тут конечно надо выбирать крипту 🤮 )))
Беспроигрышная классика инфоцыганства.

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

Скрин, в Trae -- формальная верификация протокола аутентификации Фиата-Шамира (криптографическая схема с Zero-Knowledge Proof).

Другой скрипт -- верификация эфирного смарт-контракта IERC20.sol на Solidity
(стандарт ERC20: простой токенизированный замок timelock, часто используется в DeFi для ограничения доступа к токенам на определённый период)

Вообще, этим занимаются аудиторы смарт-контрактов, средняя цена аудита на мировом рынке $20..100k. Но конкретно ниша формальной верификации (математическое доказательство безопасности) стартует где-то с $5,000–$15,000.

Например, базовый аудит простого контракта вроде токена ERC-20, критически важен, несмотря на море проверенных шаблонов (например, от OpenZeppelin). Ну потому что формальная верификация не про проверку стандарта, а про работу с конкретной уникальной реализацией. А в мире веба3 отсутствие даже базового аудита -- красный флаг ⛔️

=

Хотя на самом деле я конечно этим 💩 хуже онлайн-казино заниматься не планирую,
чисто для экспериментов, ну если вдруг какую-нибудь копеечку получится заработать как побочный эффект экспериментов, даю обет: 💯 отправляю на благотворительность.
47🤔13❤‍🔥3🔥2🐳1
Тут ещё вопрос открытый, какую сторону выбрать :)
Тёмную понятно на порядки выгоднее, но и настолько же рискованнее.

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

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

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

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

=

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

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

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

Можно запустить бобркоин для инвестирования в фейковый стартап такую пирамиду прорывную технологию.
🐳3020😁8👍6😎5
Вопрос из мейнстрима: но почему всю эту верификацию не сделать просто обычными тестами?

Главное, что тестирование проверяет, что программа работает правильно на конкретных тестовых случаях.
Например, можно проверить, что 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войства доказываются, а не проверяются;
-- структуры данных и их инварианты моделируются на уровне типов;
-- возможны автоматические доказательства и формальный анализ атак.
🤯3517🔥8👍7👏2
This media is not supported in your browser
VIEW IN TELEGRAM
Конечно, подобные сервисы имеются, крипторынок ведь мультитриллионный. Дальше разберу несколько наиболее известных.

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". А возможно кстати, сделаю формальную верификацию и моей реализации, в качестве хорошего примера.

(Размышления письмом завтра продолжу, ещё парочку фреймворков разберу, чтобы как следует эту темку продумать)
🤯35137👍1
Прувер 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 на языке со слабой системой типов и динамической типизацией предлагает более универсальную и математически более богатую среду для верификации, особенно для сложных протоколов с высшими структурами и зависимыми инвариантами.

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

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

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

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

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

=

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

Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.
👍31🤯126🔥5
В заключение сериала про инструменты формальной верификации.

Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на 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 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.

Заключительный пост сериала будет про это.
👍33🔥74😁1
Идея -- Топологически-Ориентированное Проектирование (ТОП).
На основе HoTT сделать логический фреймворк, в рамках которого можно будет формально описывать и проектные требования, и конкретные архитектурные и софт-дизайнерские аспекты.

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

И мы получим в итоге (достаточно) формальную спецификацию, на основе которой в идеальном случае можно будет автоматически сгенерировать код вместе с, например, триплами Хоара, а как минимум, будет прекрасное ТЗ для AI.

Мой курс вайб-проектирование уже неплохо работает, вчерашний отзыв:

Я прошёл курс по вайб-кодингу и сразу стал применять этот подход в одном из своих проектов в комбинации с BDD.
С помощью Qwen3 по шагам выполняю преобразования:
[ ... ]
Раньше я использовал ИИ как замену Google и StackOverflow. Теперь он превратился для меня в инструмент, которому не было аналогов. Вместо поиска информации ИИ выполняет часть работы: часть того, что он выдаёт сохраняется в проекте в той или иной форме.

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

Ключевая фишка в том, что мы делаем не просто описания тест-кейсов на Gherkin как в голову взбрело самому умненькому/опытненькому (а вдруг такого нету?), а используем для этого строго ограниченный набор инструментов ТОП.

То есть, БАЗА: по сути, мы исходно имеем набор жёстких ограничений ТОП, который нам указывает что НЕ надо делать, и таким образом пространство возможных решений сокращается от бесконечности как сегодня в мейнстриме, до очень ограниченного количества возможностей, которое просчитает любой шахматист-второразрядник.

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

То есть ТОП это по сути просто такой набор гармонично связанных мета-понятий, которые мы используем при создании Gherkin-сценариев (да или любого другого DSL, по Алану Кэю), и который по определению никогда не даст вам свернуть не туда.

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

Ну вот, навскидку, скриншоты возможных сценариев (писал AI, и на таком уровне Клод 4 например будет очень хорошим ассистентом)

(знаете кстати, как можно быстро понять что текст писал AI? он любит начинать фразы с "Это...")
29😁13🏆5💯4🤔1
Сейчас в разгаре первая волна итэ-демобилизации: стремительно исчезает вся эта беловоротничковая шушера (бухгалтеры юристы психологи администраторы дикторы телеведущие колл-центры...). Им на смену пришёл жпт.

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


Следом будет заключительная, всеобщая итэ-демобилизация: на условных "Алис" и всяческих киборгов будут окончательно заменены учителя врачи чиновники лётчики полицейские военные и спецслужбы.
Мой прогноз: до 2035-го станут естественны войны роботов (как между государствами так и между криптохакерскими структурами). Причём они будут происходить на скоростях, буквально неподвластных человеческому зрению и мышлению. Например, мириады дронов схлестнулись на доли секунды -- и уже понятно кто выиграл. Далее, соответственно, быстрый раш, только базу противника не ломаем, а захватываем.

И наконец самыми последними будут заменены программисты: потому что едва это произойдёт, что означает что AI научится кодить, как сеньор, он тут же начнёт рекурсивное самоулучшение, и просто по определению случится технологическая сингулярность.
Сроки? Максимум 2042-й год.

Думайте.
3🤯34😁25🤔9🐳7🔥6
This media is not supported in your browser
VIEW IN TELEGRAM
Не люблю и не планирую никогда учить в итэ ничему, отличающемуся от сеньорского архитекторского -- имею в виду тимлидство, техдирство и т.д., буквально зарекаюсь. И давно уже бросил консультировать, но иногда прям грустно, беспредел может быть ведь и с другой стороны.

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

Старый знакомый, сам вообще не айтишник, из военных, с инвалидностью, задумал киллер контрал-страйка (вот почему меня хотя бы не спросил? я бы прям очень жёстко сразу отговорил). Его для начала раскрутили на покупку какого-то дорогого движка за пять зелёных штук, влез в долги... Бюджет инвесторов сливается, продукт на полгода отстаёт и даже альфа-версии не видно, и уже скоро придут серьёзные пацаны с вопросом "где деньги?"...

Дорогие боссы, БАЗА: подчинённые вас в 100% наёбывают (и в принципе в 98% правильно делают, и я учу и буду продолжать, как это делать правильно, но это другое). Вешают вам лапшу насколько это трудно, сроки говорят с запасом в 2-5-11 раз, а вы мямлите "ммну ладно"...

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

Программисты должны еженедельно мучительно доказывать КАЖДЫЙ стори-поинт на общем собрании.

Не знаете что это, спросите жпт.

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

Причём это не то что "а давайте Олегу дадим три пойнта, а Оксане пять", нет.

Даже одно очко должно быть ОЧЕНЬ трудно получить :)

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

Не бойтесь, сегодня никуда разработчики не разбегутся, покряхтят и начнут работать как надо.

А вам, программисты, надо быть Человеками прежде всего (с капиталистами-то всё ясно, они по дефолту идут в ад). А не то...
👍40🫡14💯54🐳2