Просили пояснить за валютные блоги: там оказывается какая-то кривейшая платёжная система "страйп": если вы не эээ резидент и не имеете 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.

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

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

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

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

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

...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.

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

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

...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.

Однажды рано утром Бобрик получил инсайт.

"Пора наконец браться за саморазвитие! Пора начать изучать серьёзные темы -- software design, computer science!", - подумал он.

После чего перевернул подушку прохладной стороной вверх и снова сладко уснул.

Прекрасное: разработка, управляемая мазохизмом.
A masochist’s guide to web development
Пишем веб-приложение на сишечке и wasm.
emnoscripten, колбеки между си/js, многопоточность в браузере, persistent storage через idbfs... Элегантная фишка: вынос тяжёлых вычислений в веб-воркер.

2. Однажды Бобрик пришёл к старому БоброМудру и спросил:

-- Учитель! А если бы появилась теория типов ещё более сложная, чем HoTT и CoC, вы бы смогли и её реализовать?

-- Без проблем, - ответил БоброМудр.

-- Но как?? - изумился Бобрик.

-- А вот так! - ответил БоброМудр, и дал Бобрику подзатыльник.

ВайбКодинг сегодня весь день непрерывно сбоит.
Видимо, готовят мессенджер Нах.

Вчера решил обновить Нах, кнопочкой (сам он не умеет проверять апдейты), и он скачивает и запускает из самого себя полностью автономный инсталлятор. Окошечко с кнопкой скачивания, выбор каталога, весь UI -- какой-то древний стиль Delphi из 2000-х.

Так как инсталлятор автономный то он по определению не способен выбрать каталог установки, где уже размещается Нах; предлагает стандартный c: program files, тоже приходится ручками задавать,

И после чего это чудо ничтоже сумняшеся начинает установку при непосредственно работающем экземпляре Наха, ну и естественно возникает классическая проблема ↑↑↑

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

Детский сад какой-то, ей-богу.

За $1m мои ментаты сделают абсолютно защищённый и формально верифицированный мессенджер уровня телеграма (чаты + продвинутая ai-система рекомендации каналов) на 100 млн пользователей и миллион rps.

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

Уж лучше, честное слово, чем браться за что-то подобное, лучше заниматься иллюзорным стартаперством =>
"...Последние 3 недели был в Долине: полсотни встреч с стартапами и фондами, организация двух конференций, участие в пяти, два хакатона и куча эмоций.
...В городе не осталось ни одного билборда, который бы рекламировал что-то кроме ИИ. Энергия через край. Я уже писал, что в воскресенье вечером в кафе нет свободного стула, потому что все кодят стартапы. Уровень общего воодушевления выше, чем когда-либо на моей памяти."

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

Закачиваю гайд по Calculus of Constructions, много читаю по теме, вот свежачок "Programs as Singularities" университета Мельбурна.

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

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

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

Авторы предлагают т.н. "структурный байесианизм".

Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.

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

Но подход авторов нацелен конкретно на ML, и ему не хватает ни глубины, ни универсальности, ни прагматизма. Правильно это конечно делать в парадигме гомотопической теории, где геометрия проявляется через непрерывные деформации (гомотопии). HoTT уже имеет хорошо развитый аппарат для работы с непрерывными деформациями типов, понятие type identity естественно связывается с геометрической структурой, а формализовать переход между дискретным и непрерывным могут высшие индуктивные типы.

Например, алгоритм сортировки может быть представлен как зависимый тип
Sort : (A: Type) → (List A) → (List A) с доказательством упорядоченности, а нейросеть можно представить как тип NeuralNet : (Input: Type) → (Output: Type) → Type

Определяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.

Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.

Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)

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

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

Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.