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

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

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

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

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

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

Нет ничего лучше, чем постоянные громкие и нервные выкрики из своего уголка. Как автономные "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, и мы с пацанами такое сделаем.

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

Во-вторых, если серьёзно, на самом деле вы программируете на чистом функциональном языке препроцессора cpp (не путаем с c++ конечно), который состоит только из nestable expressions, которые не выполняются а оцениваются, и yields чистое значение типа Си, которое есть абстрактный тип данных (реализованный как char*). Затем это значение типа Си уже выполняется рантаймом (рантаймом cpp!), который обычно включает оптимизирующий генератор кода.

Преподобные гении Керниган и Ричи применили монады из теорката к разработке языков программирования значительно раньше, чем все остальные. Им пришлось немного прогнуться под антитеоретические штуки наподобие # undef, и правила определения области действия получились не так чисты, как, скажем, в лямбда-исчислении или Scheme (но, подождите, даже Джон Маккарти неправильно определил область действия в Лиспе.)

Следующим функциональным языком такого уровня стал Хаскель, где тип Си был сделан абстрактным ("IO"), хотя его всячески портили сектанты-вероотступники Черч, Карри и Милнер,
пока святой Wadler не допилил его до теоретически почти идеального... но по сути он остался не более чистым функциональным, чем Си + cpp.

Поэтому если хотите функциональности + мощнейшей экосистемы, пишите либо на Си под Линукс, либо на F# под .NET.
И забудьте про Java.

.

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

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

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

Засада с валидацией

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


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

Мне кажется, что ещё чуть-чуть, и продавцов курсов "за полгода на работу, зп начинающего 70,000 рублей" начнут подкарауливать на улице их клиенты...

Как только вы освоите универсальные основы разработки, создание 99% программных систем действительно станет для вас довольно простым делом. Причина в том, что всё в разработке софта сводится к трем очень специфическим вещам: [...].
...Я говорю это для того, чтобы придать вам уверенности: чтобы добиться успеха в качестве разработчика, вам просто нужно по-настоящему овладеть тремя мета-навыками ↑↑↑

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

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

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

=

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

=

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

В раздел "Элитный программист" добавлен материал
70) Шиза для программиста - 4.

В СильныеИдеи добавлен материал "120) Нечистый эффект наблюдения чистых функций".
В функциональной архитектуре (даже просто на уровне in small) чистые функции не могут выполнять "нечистые" действия. С другой стороны, наблюдение за результатом чистого вычисления будет побочным эффектом.

=

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

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

Главный приятный вывод от погружения в CoC / CIC — что она сильно ограничена узким диапазоном задач (доказательства теорем и корректности программ, верификация свойств, автоматический вывод доказательств...), на что заточены все эти европейские пруверы Coq, Agda, Idris, Lean, которым обучают всю Европу и США — и за пределы CoC они выйти не могут, чтобы стать хотя бы немного ближе к ИТ.

Поэтому как закончу "кубики", берусь за разработку думательных паттернов (мантр) in large в парадигме гомотопической теории (переводим в неё software и system design сколько получится). Ну например простейшее - вместо
"внешний ключ связывает таблицы" мы можем думать об эквивалентности путей между типами данных, выявляя некорректные или избыточные связи ещё на этапе проектирования; составные ключи — это типы h-уровней (формальный способ рассуждать о разных уровнях уникальности данных и их отношениях);
с помощью высшего индуктивного типа Pushout корректно склеиваем разные типы (результат слияния таблиц будет консистентным независимо от порядка операций) и т.д. и т.п.
Ну и сам hott-кодинг конечно (абсолютный на сегодня уровень абстракций).

=

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

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