Ещё немножко научно-популяризаторского.

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

Гомотопическая теория типов предлагает радикально новый способ мышления о сложных системах (включая прежде всего айтишные ultra-large-scale).

-- Если мы можем показать, что две различные стратегии управления роем эквивалентны (приводят к одинаковым результатам через разные пути), то унивалентность позволяет нам заменить одну стратегию на другую в любом контексте без дополнительных доказательств.

-- h-уровни:
-2 -- единственные решения -- оптимальная траектория в детерминированной среде.
Группоиды (конфигурации с симметриями) -- эквивалентные формации, отличающиеся только поворотом.
Высшие уровни -- сложные паттерны коллективного поведения с множественными уровнями эквивалентности.

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


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

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

-- Поведение роя моделируем как ∞-категорию, в категорной семантике, с поддержкой композиционного масштабирования (управление подроем автоматически композируется в управление всем мегароем через функториальность). Существующие западные пруф-ассистанты (Agda, Coq с UniMath, Lean) не оптимизированы для задач такого масштаба, и вряд ли когда-нибудь станут — из-за своей кривейшей архитектуры, написанной европейскими математиками на хаскеле.

=

Применение HoTT к построению + верификации(!) сверхсложных систем приведёт к качественному скачку в наших с вами возможностях: вместо борьбы с комбинаторным взрывом мы получаем математически элегантные способы работы с бесконечными пространствами состояний 😇

Я создаю не просто новый инструмент ТОП (топологически-ориентированное программирование) -- это будет новая парадигма мышления о сложных системах, где геометрическая интуиция и алгебраическая строгость объединяются для решения задач, ранее считавшихся неразрешимыми 💥

Но даже формальная верификация мегароя из миллионов дронов -- это лишь предвестник ещё более сложных задач грядущего будущего 💪🏻

Нигде в мире (пока) подобному не научат, а мои материалы уже частично доступны (но только моим ментатам, и только уровня Гипотетик) 🏆

А когда допилю "кубики" к этому всему, будет вообще 🔥🔥🔥

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

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

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

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

-- Предикативная иерархия упорядочивает уровни абстракции:

отдельные дроны → локальные группы → региональные формации → глобальная стратегия

что исключает "зацикливание" команд и гарантирует предсказуемое время отклика на любом масштабе.

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

-- HoTT + CTT: наш мегарой не только думает топологически (HoTT), но и действует конструктивно (CTT).

И в результате мы получаем не просто рой дронов, а искусственный сверхорганизм с математически гарантированной эффективностью 🚀🚀🚀

=

Обычный рой: локальная информация с линейным распространением, O(n) независимых решений.

HoTT-рой: глобальная информация с мгновенным распространением через эквивалентности (параллельная адаптация, все эквивалентные группы одновременно), O(log n) уровней абстракции с экспоненциальным усилением каждого уровня.

Обычный рой принимает глобальное решение за ~30 секунд, HoTT-рой ~0.1 с.
Обычный рой адаптируется к новой тактике ~5 минут, HoTT-рой ~10 с.
Обычный рой координирует маневры ~60 секунд, HoTT-рой ~1 c.

В обычном рое 60-70% дронов участвуют в оптимальных действиях, в HoTT-рое -- 90-95%.

В обычном рое потеря 30% дронов приводит к деградации координации, а HoTT-рой сохраняет эффективность при потерях до 60%.

HoTT-рой может проиграть только в случае катастрофического превосходства противника в
- скорости/маневренности отдельных дронов (в 3+ раза)
- огневой мощи (в 5+ раз)
- общей численности (в 10+ раз)

Но даже тогда HoTT-рой нанесет диспропорционально большой ущерб благодаря оптимальной тактике.

Вероятность победы HoTT-роя: 85-90%.

Это не магия, а результат математически качественно лучшей архитектуры.

HoTT превращает хаотичную схватку миллиона дронов в координированную симфонию разрушения. Это не просто количественное, а качественное превосходство в самурайском искусстве.

Придумал кстати название для будущего симулятора мегароя: СМРЙ 🤘

=

Всё, выдыхаем, всё остальное будет покрыто тайной 😎
осталась заключительная попса, нашего мини-сериала ))

В заключение попросил жпт написать несколько сценариев по моим постам =>

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

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

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


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


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


3. Мегарои сражаются за контроль над месторождениями редких металлов. Один рой специализируется на обороне - создает многослойные барьеры, минные поля из дронов-камикадзе, подземные туннели. Второй рой атакует волнами - сначала разведчики, затем подавители ПВО, наконец основные силы. Ключ к победе - логистика: кто быстрее восполняет потери и доставляет боеприпасы.


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

=

Вышел кстати очень неплохой, типа, шпионский боевик с Мистером Роботом: "The Amateur". Интересно, в США оказывается считается, что кинуть/подставить родную контору ради демократических идеалов -- это гуманистическая норма, а не предательство.
И сам сюжет сказочный и довольно линейный ("планы внутри планов" уже не котируется, нужны "планы внутри планов внутри планов "),
но Малеку очередной зачёт конечно за классную крипто-роль.

.

Облако драгоценностей за неделю.

На начальные курсы набор закрыт. Для НЕ-начинающих сегодня последняя возможность попасть в мою Лабораторию: осталось одно место, и потом закрываю до осени/зимы. DONE. Изучаете материал "Как понять в программировании всё (БАЗА)", кто его успешно осваивает, может продолжить в моей Лаборатории. Но найти это место - хардкорный квест уровня хакерских паззлов из "Quadrilateral Cowboy" (правда, в прошлый раз его нашли за 45 минут :)

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

Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).

Засада с исключениями
Засада с инициализацией
Засада с контроллером


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

(продолжение сериала)

Более совершенные инструменты разработки сделали нас более продуктивными. Но вот что это значит в эпоху AI...

...Так вот, стратегическая проблема с вайб-кодированием заключается в том, что оно не достигает вообще НИЧЕГО из нижеперечисленного...

Представьте, что следующее поколение бортового программного обеспечения и автопилота для Суперджета разрабатывается программистами по схеме vibe coding...
7 рекомендаций, где начинающим лучше использовать AI.

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

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

СильныеИдеи++
41. SOLID25 : [1...]
Хорошо, SOLID мы захейтили, но не предлагать работающие альтернативы было бы неконструктивно. В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.

Продолжение трека "Элитный программист":
28) Практика ведения дискуссии с несогласными людьми.
Когда вы ведёте переговоры о зарплате, вы по определению сталкиваетесь с противником — с теми, кто хочет, чтобы она была как можно ниже. Для вас это доход, а для вашего работодателя или клиента это расход. Поэтому необходимо уметь связно излагать свою позицию и справляться с возражениями...

Как я перестал беспокоиться и начал счастливо кодировать.
Практический совет и 5 рекомендаций по AI-IDE...

Тестируем на практике 4 нейронки: подробный гайд, когда же жпт заменит сеньоров-архитекторов.

=

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


=

Гайд "Гомотопическая теория типов для программистов (2)":
этим летом 💯 будет готов.
Взялся за "Кубическую теорию типов для программистов",
этим летом/осенью 💯 будет готов.

И потом стану думать над симулятором мегароя (тренажёр HoTT), но доступен будет только моим ментатам, и только уровня Гипотетик.

=

Трек "Чистое Проектирование/Software Design in Large", материал "Ясная архитектура"

Добавлен разбор реализации "15. Event Sourcing"

=

Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 17 уровней из ~50 альфа-версии.
этим летом бета-версия 💯 будет готова.

p.s. Сергею Бобровскому респект за второй подряд кубок Стэнли 🏆

Когда в понедельник локально отладил тикет, и вечером пообещал тимлиду, что "завтра задеплоим!".

Вы же понимаете, что и язык квантовых вычислений Q#, и функциональный Erland в акторной модели -- это никакие не разные парадигмы, а просто симметричная моноидальная категория ?

Вот только чтобы понять это, надо сперва осознать, почему Q# и Erlang -- разные парадигмы и качественно разные вычислительные модели.

ВШЭ подняла цену на обучение, внимание, прикладной математике! (этому реально трудно учиться, по себе знаю 💪🏻) с 467 до 767 тысяч рублей за год учёбы.
Но главное конечно, что спрос на эти темки ощутимо растёт, и это прекрасно ❤️

Даже, думаю, стратегически, на 51% сместить акцент на математику, конкретно в контексте программирования конечно, но всё же по достаточно серьёзным темам 🤓

Вчерашний отзыв от ментата, приближающегося к уровню Гипотетик (подготовительное перед гайдом по гомотопической теории 🚀):

Я прочитал книгу "Типы в языках программирования" (Пирс).
Особенно интересными для меня были следующие моменты:

1) Константы Чёрча в лямбда-исчислении.
Всегда воспринимал константы как "атомы", а оказалось, что их можно составить из более низкоуровневых конструкций.

2) Соотношение Карри-Говарда между логикой и типами.
Вот, оказывается, как теория типов связана с доказательством теорем.

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

p.s. Хотите, индивидуально буду обучать по курсам вшэ, мехмата, физтеха, спбгу? mit, cmu, оксфорд гарвард :)

❤️❤️❤️

Риторическое.

1. Почему национальный менеджер называется по-английски MAX (сразу в нарушении нескольких законов) ?

2. Но даже если как его иногда пишут МАКС, нарушается правило русского языка в отношении имён собственных (которое изучается во втором классе началки): имеет право только начинаться с заглавной буквы (например, Макс), а лепет про "ну ммм ээээ а это у нас вот такое название крупненьким пишем, вот у нас так принято" отдел маркетинга может засунуть себе ... ?

Просили пояснить за валютные блоги: там оказывается какая-то кривейшая платёжная система "страйп": если вы не эээ резидент и не имеете ein, то фиг там зарегитесь. Действительно даже если у вас счёт в крупном западном банке (не американском), то всё равно совсем не факт, что сабстэк вас застрайпонит: потребуется скорее всего предоставить инфу о юридическом статусе и т.п.

При том что есть шикарные аналоги -- например Ghost, который превосходит Substack по возможностям на порядок.

И тем не менее это очень наглядный пример того, что сабстэк в текстовых блогах сегодня как ютуб в видео: какие усилия не прикладывай, теперь уже в принципе не догнать даже на 2%.

Это уже огромное количество контента, тесно связанное с системой рекомендаций, кросс-постингом и множеством других инструментов, которые упрощают органический рост.
(а у нас ВК обрезает охваты теперь вообще до нуля... вообще, законодательно надо их обязать, коли монополисты, гарантированный показ каждого поста всем подписчикам в течение 48 часов.)

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

Надо работать на более высоком уровне абстракции, и в первую очередь определить свою ПЛАТЯЩУЮ ЦА.

Звезда современного бурлеска Дита фон Тиз однажды рассказала, чему она научилась в самом начале своей карьеры стриптизерши в Лос Анджелесе. Ее коллеги – пергидрольные блондинки танцовщицы с искусственным загаром, бразильской эпиляцией и в бикини неоновых цветов – раздевались догола, если в клубе было пятьдесят мужчин, и каждый из них давал им по доллару. Дита появлялась на сцене в атласных перчатках, корсете и пачке, исполняла зажигательный танец и раздевалась до нижнего белья, чем приводила зрителей в недоумение. Но после этого, несмотря на то, что сорок девять мужчин ее игнорировали, находился один, который давал ей пятьдесят долларов.
Этот мужчина, по словам Диты, и был ее аудиторией.
Тим Феррис, "На плечах гигантов"

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

В основу своего петушка Кокан заложил собственную теорию типов Calculus of Constructions (CoC): типизированное λ-исчисление + логика высшего порядка + полиморфизм, через изоморфизм Карри-Ховарда.
И это конечно топчик λ-куба Барендрегта, да, но...

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

В CoC равенство определяется через лейбницевский принцип неразличимости тождественного. В HoTT он заменяется на тип путей Path (непрерывная деформация), а доказательства равенства становятся конструктивными (например, гомотопии), что позволяет естественно кодировать высшие категории или ∞-группоиды например. При этом сохраняется canonicity: программы на основе HoTT можно выполнять, а доказательства верифицируются алгоритмически.

хотт - это язык программирования Бога

Владимир Воеводский реализовал свои гениальные идеи HoTT в библиотеке Coq через расширение CIC (Calculus of Inductive Constructions). Он по сути трансформировал применение Coq, показав, что формальные системы могут кодировать не только логику, но и глубокие геометрические структуры.

Но в итоге два ведущих теорем-прувера + языка с заптипчиками - Coq/Rocq и Lean - решили развиваться в направлении усиления CIC, и по сути отказались от HoTT в своих движках, во многом из-за их архитектурной кривизны. По большому счёту это стратегическая ошибка, пояснял тут.
И это прям очень-очень радует 💥💥💥

-- Сергей Игоревич, меня иногда спрашивают "а зачем ты это всё учишь?" (например, математику), и я не знаю что ответить.

Честно, я сам даже не знаю, что ответить на вопрос "что ответить?", для меня это просто Кэп Очевидность.

Я например всю жизнь учусь для того чтобы становиться умнее, и это мне очень здорово всю жизнь помогает. И для меня вообще очень странно, что может быть по-другому.

Ну, да, у тех, кто задаёт вопросы "а зачем учиться [чему угодно]?", с развитием умишка как раз по определению большие проблемы. Глупенькие просто по жизни.

Можете ответить так например: "количество извилин в мозгу у определённых групп людей различается столь сильно, что это по сути формально разные виды животных". Ну как минимум, разные касты.

Лайфхак если вас возвращают в офис с удалёнки, или вообще работа представляет собой концлагерь опенспейса.

Нет ничего лучше, чем постоянные громкие и нервные выкрики из своего уголка. Как автономные "WTF???", регулярно отвлекающие соседних коллег (матюшки тоже хорошо заходят, можно также позаикаться для особого нервирования окружающих), так и вопли на другой конец:

-- Олег, ... твою мать! Какого хера ты возвращаешь 500 на мой огромный джсон?

На каждую просьбу менеджеров "потише пожалуйста!" отвечайте одной и той же фразой "Хочите тишины? Возвращайте удалёнку, а я по другому не умею работать".

На "общайтесь в чате" -- "а нафига тогда нас призвали в офис??".

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

Можно также приходить в вызывающей одежде (шорты и шлёпки прям топчик будет).

.

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

Нужнейшее на выхи: поиграть в правильные игры. Прочитал что (якобы) в Казахстане хотят запретить все игры кроме развивающих образовательных и пазлов, дико поддерживаю 💯
Ну может быть не столь категорично к этим жанрам добавить ещё небольшой "белый список": дота2, dune 2, starcraft ][, assetto corsa и dune awakening (ну ладно, и контру:).

А так, 99,999% всего этого геймерского кала. включая приставки всех видов 💩 в топку, и вместе с ними забанить и все эти онлайн-кинотеатры с бесконечным киносериальным мусором 🤮 (да ещё и укравшие у народа ЛЧ ⚽️).

=

Вот белый список (lvl 1) разрешённых игр Лаборатории, которые каждому ментату абсолютно обязательно пройти до конца.

1) Развитие топологического мышления.

- Monument Valley все серии (22 июля выходит v3, срочно ставим в вишлисты);

- The Bridge (я иногда думал, ну вообще невозможно)

2) Развитие мета-мышления.

- Baba Is You

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

вот один из сотен анти-примеров: в idle-играх гигантские чиселки это норма например, но BigInteger поддерживает только целочисленное деление.

BigInteger x, y;

x / y — как это сделаешь?

double result = (double)x / y; // <= детский сад; в дабле мантисса 53 бита

double result = Math.Exp(BigInteger.Log(x) - BigInteger.Log(y));

Я исходно взял decimal (10^28 с точностью 100%), хотя сразу сильно сомневался, и не зря: для ачивки "Архитектор Цифровой Реальности" например потребуется 50.000 октиллионов (и это далеко не предел; после нескольких взломов Матрицы счёт крипты пойдёт на вигинтиллионы).

Как обычно надо было следовать собственным рекомендациям с "Быстрой прокачки ООП": любой сомнительный базовый/стандартный тип надо сразу же оборачивать своим типом во избежание. А в результате 2 часа рефакторил, и снова надо тестить нюансы.

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

Ведь логарифм — это просто изоморфизм между мультипликативной группой положительных чисел и аддитивной группой вещественных чисел...

...Так вот чем в итоге ожидаемо закончился весь этот хайп "AI скоро заменит программистов": жпт просто стал must have скиллом, наряду с каким-нибудь кубером, который ранее был отдельной профессией; от программистов на работе стали требовать уметь и делать в x10...x100 раз больше, а зарплаты при этом даже немножечко понижаются.

А с другой стороны...

Пол почувствовал, что опять угодил в слепое время...

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

-- Этому не бывать, - прошептал он. -- Я не допущу.

.

Облако драгоценностей за неделю.

Набор ментатов в Лабораторию на 2025-й год закончен.
(регулярно думаю о том, как становиться меньше и постепенно исчезать из Сети)

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

Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).

Засада с микросервисами

Предыдущие серии:
Засада с исключениями
Засада с инициализацией
Засада с контроллером


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

...Вопрос уже не о том, заменит ли нас искусственный интеллект, а в том, кто быстрее всего освоит искусственный интеллект своих целях. И одна из недооценённых областей интересов, о которой, как мне кажется, говорят недостаточно — это ОБРАЗОВАНИЕ.
6 рекомендаций + промпты для начинающих и всех желающих продуктивно самообучаться.

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

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

СильныеИдеи++
42. SOLID25 : [2...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.

Продолжение трека "Элитный программист":
29) Как соцсети помогут вам в создании личного бренда.
Вы можете быть элитным программистом с отличными навыками общения и работы в команде, но если ваши публичные профили в соцсетях выглядят плохо, никто не захочет брать вас на работу...

Золотые правила карьеры разработчика.
1. [...]. Идеальный вариант, когда тратишь на рабочие задачки по удалёнке 4 часа в неделю (включая все созвоны), но зарплату получаешь на постоянке.


=

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


=

Новые материалы для ментатов Лаборатории.

В раздел "Элитный программист" добавлен материал
69) Шиза для программиста - 3.
База для тех, у кого проблемы с внимательностью к коду и его логике.

В курс карьеры добавлен 101-й материал "Софт-скиллы или хард-скиллы?".
Это вечный вопрос, и на него есть однозначный ответ.


=

"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.

Гайд по "Calculus of Inductive Constructions",
этим летом 💯 будет готов.
(я решил сперва сделать λ-куб Барендрегта)

=

Трек "Чистое Проектирование/Software Design in Large", материал "Ясная архитектура"

Добавлены все планировавшиеся архитектуры 16-22:
Stream Processing, две расширенных архитектуры на монадах состояний с обработкой ошибок и абсолютной безопасностью, интерпретатор AST, пишем DSL, абстрактный тип данных.

На неделе оформлю в дополнение к действующему материалу ЯА, кто из ныне действующих ментатов в 2025-м ранее изучал, можете бесплатно допройти.

=

Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 20 уровней из ~50 альфа-версии,
переделал на BigInteger, добавил много ачивок и мотивирующих бонусов за различные схемы делания помидорок,
этим летом бета-версия 💯 будет готова.

20-й лвл:
Проникновение в ядро городской операционной системы (Центр Управления Мегаполисом) или его критически важные модули. Кража шифровальных ключей; доступ к архивам всех городских систем; внедрение постоянных бэкдоров; тотальный мониторинг инфраструктуры; попытка перезагрузки секторов.
Мой чип — украденный прототип ЦЕРНа. Ломает банковские SSL за 0.3 нс.

Немного поигрался с лямбда-кубом Барендрегта, пошёл сверху вниз:
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.

Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.

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

А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....

все уснули давно
в километрах глубин
никого ничего он остался один....

кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...

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