Я закончил второй гайд по гомотопической теории ↑ ↑ ↑

И сразу взялся за "кубики", ещё шесть лет назад планировал.

Казалось бы, да ну чего там, эх! в сравнении с HoTT в CTT база чистая геометрия: куб, грани, интервал (1-куб), направления, system, и потом сразу заходим на открытые боксы в кубическом типе...

ага, щас, за 4 часа слил сотку баксов на клода4 и крепко наполучал граблями по лбу; cхема классов вроде бы очевидная, но внутри там такие хардкорные математические завязки...

Начал всё переделывать с нуля по взрослому, в соответствии со своими собственными рекомендациями по проектированию :)

свежий отзыв на материал по вайб-проектированию:

"Я вчера добил ваш [...] по Vibe Coding – хороший материал, и востребованный, в том смысле что до сих пор удивительно много разработчиков которые вообще не пользуются LLM для ускорения своей работы
Конечно, одно из самых ценных что вы упоминаете это тестирование, это надо выделить красным огромным заголовком вообще, потому что прочитают и забудут, и не будут тесты никакие нормальные генерировать (в cursor это вообще надо прям в cursorules наверное прописывать)."

Да, ну там всё же основной акцент на software/system desing, тесты это действительно просто техническое must have (хотя для AI мы формулируем их как спецификации), необходимость которых даже и упоминать странно в контексте AI.

=

Ладно, я реализацию HoTT только на 5-7-й итерации смог сделать, а CTT вдобавок действительно немного необычная, много топологических нюансов. Суммарно обе эти теории, подозреваю, в тысячу зелёных обойдутся 🙈

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

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

Как заработать 1 млн долларов за год? Ну, это простая математика:

60 x 60 x 24 = 86 400 секунд в день
86 400 × 365 = 31 536 000 секунд в год
1,000,000 / 31,536,000 = $0.0317

Вам просто нужно зарабатывать 300k/s $0,03/s , или 2-3 рубля каждую секунду,

И вы только что влезли в долги на 20 рублей, читая это.

То странное чувство, когда последовал своим собственным рекомендациям из курса по вайб-проектированию, и вместо 100 долларов на первую неудачную итерацию теперь потратил всего 5, а получил полноценную реализацию первых базовых понятий CTT, причём с полного нуля и вдобавок с готовой спецификацией для последующей работы.

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

И по мере того как изучаю это всё, открываются весьма неожиданные темки в плане применения движка HoTT+CTT: верификация квантовых алгоритмов в принципе ещё где-то на первых, поверхностных уровнях пространства понимания.

=

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

Вы же читали профильную классику -- "Непобедимый" Лема, "Рой" Стерлинга, "Муравьиная ферма" Фрэнка нашего Герберта? Ну вот она уже тут. По Лему кстати пару лет назад вышла шикарная игра "The Invincible", собравшая кучу призов.
(Кстати, а почему у нас игры по Беляеву например не делают? у него в книгах множество абсолютно уникальных идей; или Ефремов; я уж не упоминаю Б.С. ...)

Но структура такого мегароя -- не просто большое число, это качественно новый уровень сложности. В нашем мозгу всего-то 80+ миллиардов нейронов, но они не летают в трёхмерном пространстве и не рискуют столкнуться друг с другом на скорости 20 метров в секунду. Для сравнения, современный игровой движок даже просто коллизии простых сфер потянет, ну может сотню тысяч для нескольких тысяч объектов на кадр. А если меши, так вообще штук сто на 10 тыщ коллизий. А если continuous collision detection требуется?

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

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

При этом управление таким мегароем имеет на сегодня абсолютные объективные физические ограничения. Сто белковых операторов, каждый со своим дроном, и каким-то более-менее централизованным управление командой -- ну наверное. Тысяча? Уже начинается куча организационных вопросов. Миллион — ну наверное для каких-то азиатских стран. Но как ими управлять-то? Иерархическая схема здесь не работает, требуется именно что-то горизонтальное — но возникает куча не только организационных но и технических засад (лаги, связь, полоса пропускания...).

AI? Но система управления мегароем не может быть централизованной в принципе: никакой компьютер не сможет в реальном времени обрабатывать информацию от миллиона агентов и выдавать им индивидуальные команды (экспоненциальный рост пространства состояний).

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

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

При этом мы должны обеспечить:

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

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

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

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

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

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

(Какая классная игра-симулятор + хотт-тренажёр получается :)

=

-- Но, Сергей Игоревич, если вы создаёте мегарой под управлением продвинутой математической теории, разве всё равно не будет вероятность победы 50 на 50? Ведь каждый дрон фактически просто будет атаковать ближайший дрон противника, равный ему по силам?

Ok, поясню далее, какое непреодолимое преимущество в данном случае даёт HoTT + CTT.

.

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

Каждое состояние миллиона дронов -- это точка в многомерном пространстве; HoTT позволяет работать с целыми областями этого пространства как с едиными объектами (гомотопическая эквивалентность).

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

=

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

Ключевое преимущество HoTT: композиция типов автоматически обеспечивает композицию свойств.

Детали раскрывать не буду, вот навскидку:

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

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

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

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

-- [...] "свёртывает" видимое поведение к ловушке (например, часть роя имитирует преследование, основные силы готовят контрудар).

-- [...] мгновенно "склеивает" разрозненные группы в новые боевые формации: даже физически разделённые части действуют как единое целое.

Пока я нашёл семь таких ↑↑↑ гомотопических автоматов для моделирования мегароя.

Размышления продолжаю :)

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

(потерпите пожалуйста 🙏🙏🙏 , ещё 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 в своих движках, во многом из-за их архитектурной кривизны. По большому счёту это стратегическая ошибка, пояснял тут.
И это прям очень-очень радует 💥💥💥