Лаборатория Математики и Программирования Сергея Бобровского

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

Первые простенькие пруф-ассистанты появились лет 15 назад после гениальных работ Воеводского, и ими пока вряд ли даже 2% профессиональных математиков пользуются (в силу врождённого снобизма:). Ну и как работают классические математики? Представьте, что вам надо спроектировать систему на 400 таблиц исключительно на листочках бумаги, а затем писать к ней сложные SQL-запросы, моделируя их работу тоже в голове -- но получить в итоге абсолютно корректный и гарантированно работающий код.

Конечно их труд будет крайне медленным. Terence Tao кстати дал в своём блоге отсылочку на свежий правительственный грант "Exponentiating Mathematics (expMath)"
(который на самом деле выдвинуло военное агентство передовых исследований DARPA :).

MATHEMATICS IS THE SOURCE OF SIGNIFICANT TECHNOLOGICAL ADVANCES; HOWEVER, PROGRESS IN MATH IS SLOW. Recent advances in artificial intelligence (AI) suggest the possibility of increasing the rate of progress in mathematics. Still, a wide gap exists between state-of-the-art AI capabilities and pure mathematics research.

А по мне, так математиков просто надо принудительно учить программной и системной инженерии.

=

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

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

Главная теорема → Дополнительные теоремы (например, оценка энтропии) → Леммы (например, свойства аддитивных множеств) → Тактики Lean

Вот какая структурная аналогия (гомоморфизм) получается для нас:

Система → Модули → Функции → Типы данных (тайп-чекеры...)

Так вот что здесь ключевое: декомпозиция дополнительных теорем на леммы.

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

Но как?? Это ведь по сути ключевой момент programming in large, но этому не учат вообще нигде.

Почему, "поясняет" и Тао, и классические книги по математическому мышлению: потому что никто не знает как.

И начинается вечная песня: это только опыт и интуиция бла-бла-бла.

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

Ну и? Одна вода.

продолжение следует

Поизучал ночку блоги филдсовского лауреата Terence Tao, его научные труды, стримы с вайб-кодингом на Lean, повспоминал других аналогичных топовых пацанов в теме,
за которыми слежу не один десяток лет, и вот что могу вам сказать, дорогие:

Математика существенно проще, чем программирование.

Даже на уровне миддлов. Сеньор с хорошим образованием в информатике вообще без проблем впишется в ряд cчитающихся сложными математических тем, но даже продвинутый PhD будет сильно страдать на джуниорском уровне.

Это не программисту надо знать математику, а математику надо знать программирование.

Когда я делал реализацию HoTT, местами регулярно удивлялся, ну это же в принципе вещи достаточно простые. Ладно, видно я просто чего-то не понимаю....

Пока на блоге Тао не словил инсайты.

=

Тео регулярно хайпует упоминает проект формализации гипотезы Polynomial Freiman-Ruzsa (актуально в частности для криптографии: анализ псевдослучайных генераторов), доказательство которой было декомпозировано АЖ на 512 лемм, каждая из которых проверялась в Lean независимо.

Думаю, что многие из вас посмеются. 500 лемм считай -- это 500 функций/классов, пусть даже с хорошими спецификациями с TDD, с пред- и пост-условиями после BDD. Это просто уровень крепкого миддла.

Причём это не притянуто за уши, это реально глубокая аналогия.

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

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

И вот дальше начинается САМОЕ интересное и важное....

продолжение следует

Наблюдаю, как массово репощут какие-то глупенькие посты, что дескать, смотрите, аж целый филдсовский лауреат (это как нобелевка, только в математике) Terence Tao пишет код с помощью жпт, и у него всё отлично получается. И какие-то мутные скриншоты "в подтверждение", которые на самом деле из его видео "Formalizing a proof in Lean using Github Copilot only", где уже само название как бы намекает, что "это другое". Вот тут код с его стрима: Lean formalization of asymptotic estimates

Тао занимается этим уже давно, в частности, в рамках фонда "AI for Math fund" разрабатывает AI-модели для автоматической формализации доказательств (ну, да, вайб-кодинг, но на функциональном языке Lean с завтипчиками) и генерации тактик для пруф-ассистантов, включая метаматематические подходы, и вообще очень активно занимается развитием Lean. Тао также создаёт интерактивные учебники -- как детализировать доказательства "до аксиом" через Lean, и т.п.
Почитайте его блог, увлекательно.

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

Трудится Тао на гранты Национального научного фонда США, техногигантов уровня Гугла, заинтересованных в ликвидации всех программистов формальной верификации кода, а также увы увы ряда откровенно недружественных структур.
Одна из тем его исследований например -- компрессионное зондирование (compressive sensing - восстанавливаем сигнал по его истории), актуальное для радиоэлектронной разведки, взлома спецсигналов номерных радиостанций...

Но, думаю, на 80-90% его деятельность публичная, за что ему дикое уважение.

У нас, вот конкретно что по темке Lean или Coq по профилю Тао? Какие-то фрагментарные исследования, единичные энтузиасты, в основном чистые математики, существенное отставание от США, нулевое финансирование, тотальная утечка кадров... Ни блогов на русском, ни гитхабов. Какие-то полудохлые чатики в тг, где одна вода, и всё.

При том, что любимая Российская Федерация и по сей день отличается сильнейшей в мире абстрактной математикой благодаря глубоким традициям математической логики (Школы Колмогорова, Лаврентьева, Маркова...).

=

Я кстати в сентябре 24-го думал "запилить hott-плагин для Lean", но у меня старенький комп особо не тянет Lean даже без AI :)
Вот тут: "Термы -- это деревья, а деревья -- это термы"
А для задач уровня Тео надо уметь перемалывать/переписывать десятки, сотни миллионов термов.
Мои тогдашние оценки:
"...vds с озу 200 гиг под подобные задачки стоит дороже, чем дедик, меньше $100/месяц не получается...
Рабочие станции Dell 7920, HP Z8 G4, Lenovo P920 (потенциально терабайты оперативки) продаются с 16 гб (!) от трёх тысяч долларов (а серваки уже от $5 тыс)."

=

Ладно, всё равно никому это не нужно. Доделываю курсы по базовой теории HoTT на Lean питончике (на которые впишутся два с половиной курсанта, но и этот будет хороший результат), потом подетальнее поизучаю, что такого Тао делает в плане обучения формальным подходам, и попробую его идеи как-то отмаппить на топологически-ориентированное проектирование. А вдруг?

Отчёт за неделю.

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

"С тех пор как я начал использовать ЖПТ, я внезапно понял, что потерял способность программировать без него! Я смотрю на очередной рабочий тикет в ситуации, когда интернет не доступен, и в ужасе чувствую, что не представляю, как его реализовать!.."
Тотальная паника!

"Без паники! Всё будет хорошо! Даю слово!" 😁

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


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

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

Никогда ещё в истории ИТ не было БОЛЕЕ ЛУЧШЕГО момента для того, чтобы "войтивайти", чтобы стать младшим разработчиком, чем сегодня, в 2025-м году ...


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

СильныеИдеи++
Мы закончили разбор принципов SOLID с точки зрения функционального программирования. Далее будет серия материалов, в которых мы будем SOLID жёстко хейтить :) И после неё рассмотрим в отдельном сериале, какие правильные - взрослые - инженерные подходы пришли на смену SOLID в 2025-м году.
36. Жёсткий хейт SOLID | SRP
Давайте ещё раз взглянем на эти пять принципов, каждый из которых опровергнуть, как оказывается, даже легче, чем кажется изначально (ну разве что кроме LSP).
Собственно, альтернатива во всех случаях оказывалась одной и той же ...

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

Бусти: закрыт.
Выложен предпоследний материал "System Design Blueprint: The Ultimate Guide", классная компактная выжимка по теме (с картинками:)

=

Новые материалы для курсантов.

В раздел "Элитный программист" добавлен материал
66) Два важных исследования состояния потока.
Исследование ... , в котором приняли участие сотни игроков в настольные игры, предполагает, что длительное комфортное нахождение в потоке может быть обусловлено небольшим ...

В "Бесстрашные переговоры о зарплате" добавлен материал
54) Ваша базовая манипуляция для переговоров.

=

Курс "Гомотопическая теория типов для программистов: ТОП (Топологически Ориентированное Программирование)". Часть 1.
"После майских" курс 💯 будет готов.
К лету курс 💯будет готов.
Переношу все материалы обратно на мою аутентичную учебную платформу, фактически уже заключительный процесс - форматирование курса.
Всего где-то 50-60 топиков, задеплоил 10.

Хвалёный дипсик с дипсинком не смог асилить 40 строк кода на пыхапы, бесит прям :)

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

Напомню в 100500-й раз себе и остальным, что работать с ЖПТ нормально можно только через TDD (в крайнем случае бэби-версия "тесты первыми"). Иначе так и будет постоянно как сегодня или вчера.

Несомненный плюс чистого TDD также и в том, что от белкового требуется хорошее понимание домена (в частности, типовых use cases), а Red очень хорош тем, что мы не только формулируем конкретные ожидания, но и ассертами явно указываем их спецификацию (что мы хотим получить, а не как), защищаясь от ложно-положительных результатов. Я именно так и делал реализацию HoTT, поэтому и получилось норм.

Мантра: если ЖПТ предлагает код до написания теста -- удалите его и начните с Red.

Ну и мой курс по TDD в помощь.

Сколь бы не были сильными абстракции уровня programming in small

(как я например использовал для демонстрационной игры Змейка -- самые сильные на сегодня в математическом смысле),

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

Форматирую для курса код Змейки, который нагенерил
"...в полностью агентных задачах лидируют SWE-Agent, Github Copilot (VSCode), Windsurf - почти все на базе нашей любимой Claude 3.7 Sonnet."

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

Глаз зацепляется вот за такое:

def toggle_pause(self, state: GameState, engine) -> GameState:
        engine.toggle_pause()
        return state

WTF??

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

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

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

Но зато на удивление естественно и продуктивно в вайб-проектирование укладывается мой трек по ООАП: я сейчас рекомендую всем, кто прошёл с него третий курс (делаем проект по предлагаемой методике), перепройти его заново уже в связке с AI и с учётом новых рекомендаций.

=

А главный вывод в том, что, как закончу второй курс по базовой теории HoTT, надо будет думать прежде всего в направлении топологически-ориентированного проектирования: как всю эту могучую силушку гомотопической теории типов залифтить до programming in large.

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

Но это всё остаётся всё же какое-то половинчатое programming in large in small. Можно например попробовать кодировать бизнес-правила и ограничения как "пути" между зависимыми типами...

Пока не знаю, размышления продолжаю.

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

Смешное: как пацан джва года пилил игру на Rust, а потом психанул, и за шесть недель переписал всё на C# и юньку, и наслаждается комфортом.

Причины из материала, по которым Rust не покатил:
- сложность быстрого прототипирования;
- проблемы с обновлениями движка Bevy и API-дрейфом;
- ограниченная поддержка AI-инструментов для Rust.

Rust даёт нам как бы мемори сэйф, но напрочь отнимает безопасность психики :) Шарпик хотя бы оставляет нормальный рассудок. А Unity как старый добрый дедушка: периодически ругается, но хотя бы предсказуем.

Но в целом я однозначно за изучение Rust, если вы пишете на Си/С++, да ещё и работаете в геймдеве, или разрабатываете что-то системного профиля. Сильное подозрение, что жпт ещё долго не будет тянуть Rust, и порог входа в эту тему останется достаточно высоким, что 💯 хорошо в плане нишевых вакансий и продвинутых зарплат.

🔥 Мой мидл-лайф на Java & Spring (зумер-версия) 🔥

Прикиньте, я — программист-зумер ☕️ (уже мидл, но в душе джун). Пишу на Java (олдскул, но с вайбом).

Мой стэк:
✔️ Java (80% времени гуглю "как избежать NPE");
✔️ Spring (аннотации — это магия, а @ Autowired — моя религия);
✔️ Hibernate (иногда ленивый, иногда — нет, как мой кодревью).

Как я работаю:
1️⃣ Открываю IntelliJ IDEA (без джетбрейнза — как без души);
2️⃣ Запускаю Spring Boot (жду 5 минут, пока бины протрезвеют);
3️⃣ Пишу код (но сначала спрашиваю у Copilot 🤖);
4️⃣ Ломаю прод (но чиню до того, как тимлид открывает Jira).

Мои эмоции:
✅ Тесты прошли с первого раза? Я — гений 🧠✨;
❌ Упал прод? "Это баг в Spring, не мое" 🐞;
👀 Вижу legacy-код? "Ктоэтонаписал?!" (потом вспоминаю, что это я).

Моя философия:
🔧 Работает? Не трогай.
♻️ Не работает? mvn clean install.
💥 Совсем не работает? Перезапусти IDE.

Вывод:
Я — мидл, но чувствую себя сеньором (пока не спросят про транзакции).

P.S. Если код странный — это не баг, а фича 🚀

#Java #Spring #ZумDev #МидлНаМореКофе

Продолжаю работу с курсантами 🤓

Cегодняшнее:

...Недавно у меня была аттестация в компании. Менеджер сказала, что заказчик доволен моей работой, но не готов пока повысить мою ставку, и поэтому компания не может повысить мне зп. Что рассмотрят повышение в июле. Для меня это было неожиданно, и я спросила, а на какое повышение могу в принципе рассчитывать. Менеджер замялась, сказала что не хочет ничего обещать, но возможно 10%.
Вообще, это для меня первый опыт переговоров о повышении, судя по всему, я довольно слабо их провела. К июлю планирую применить рекомендации из "Курса Карьеры", чтобы быть более подготовленной.
...Но есть и плюс, компания одобрила и готова оплатить мне сторонее обучение по архитектуре.

Ситуация кстати довольно типичная: вами во всём довольны, но денег нет "по независящим причинам". На самом деле это враньё: если видят что человеку можно просто не заплатить, то и не заплатят. Но при этом за рост ваших скиллов, чтобы вы работали в разы продуктивнее, они платить готовы :)
Дело не в слабых переговорах, а в отсутствии системного подхода. Эту тему надо регулярно прокачивать, начиная за полгода минимум до аттестации. Как это делать, я подробно разбираю на треке БПЗ.
+10% это конечно вообще ни о чём: если за год зп не вырастает хотя бы на 20-25% (стандарт 2x15%), значит далее будет только хуже.

...Индексацию з/п не проводили с начала СВО. В этом году планировали, разговоров было сверхмного, а в результате выделили три копейки в масштабах всей организации. У нас руководство вообще не поняло, как поделить эти деньги. В результате, увеличили всем оклад на одну тысячу рублей. Очень многие сказали "а, ну хорошо" и сейчас прямо на работе ищут работу.

Майское:

...Вот и последствия длинных выходных)
уже успел забыть происходящее

...За 3 года на работе понял, что заблуждался по поводу прокачки и роста, у меня есколько поменялся взгляд на разработку, некоторые вещи, которые раньше казались важными, перестали таковыми являться сейчас. Через некоторое время я освоился с рабочими задачами и стремительный рост прекратился. Заниматься дальше на других курсах я не стал. Были разные жизненные ситуации, из-за которых очень легко было оправдывать своё бездействие в плане учёбы. Сейчас я понимаю, что так продолжать нельзя, ибо этот путь приведёт на обочину IT-мира. Нужно учиться, чтобы оставаться на плаву и достигать новых высот. С начала этого года решил взять за ум и
Ещё ощутил важность хорошего проектирования. На работе поручили создать новый сервис и я испытывал дискомфорт, от того, что толком не понимал хороша или плоха моя архитектура, как нужно делать, а как – нет.

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

...Сходил на собес к производственнику и попил кофе после тренировки с владельцем небольшой фирмы, которая делает беспилотники. У них типа кадровый голод, готовы платить 250+, но опытным спецам в их стеке (у первого какие-то нейросетки для оптимизации производственных издержек , у другого микроконтроллеры и си / ассемблер).

...недавно я написал сообщение в соответствующем канале, запрос продукт менеджерам на тестирование беты ассистента, где было всего лишь 4к знаков, ничего лишнего (даже картинка была с пояснением для совсем имбецилов), короче - подробный запрос на то что просим протестировать, чего ждать и чего не ждать от системы, и в каком формате мы настоятельно просим оформить фидбек. - Полный провал, 1 из 3 продактов смог 2 сообщения написать вменяемо (и видимо таки прочитал сообщение) остальные - я не знаю, не хочу ругать людей, но не могу не ругать - откровенные идиоты

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

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

А на первом курсе в заключение пишем реалтаймовую Змейку полностью в топологический-ориентированном стиле, на нашем HoTT-движке.

Для моделирования топологии игрового поля используем n-мерный тор (n=2 :).
(автоматическое применение правил оборачивания границ, характерных для тора)
Для представления координат и состояний - Product-тип.
Для моделирования направлений и игровых событий - Sum-тип.
Для отслеживания движения и проверки столкновений - гомотопические пути (Path).
Для представления действий, не возвращающих значимых результатов, таких как пауза или сохранение игры - тип Unit.
Для функций обработки ввода/вывода -- Pi-тип
(зависимая типизация, где для каждого значения домена (нажатия клавиши) определяется функция, преобразующая игровое состояние с учетом текущего контекста).

Сама Змейка
- использует Sum для представления направления движения;
- возвращает Path для отслеживания траектории;
- хранит историю движений как последовательность путей;
- методы проверки коллизий возвращают Sum-типы.

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

=

Какие мощные плюсы мы имеем уже даже на таком уровне в сравнении с ООП?

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

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

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

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

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

Бонус: AI очень даже хорошо рассуждает на таком уровне, поэтому потенциально вполне можно формализовать в ТОП и TDD, и BDD.

...И в то же время, хотя это всё может дать невероятную продуктивность - десятки, сотни раз! -- этим практически никто не занимается. Даже не математика и tcs, а достаточно рядовые достижения cs и программной инженерии.
Никому особо это не нужно, как неуловимый Джо. Парадокс?

А вы спросите у своего техдира, сколько он готов заплатить за услугу, которая гарантированно ускорит выпуск фич например в 42 раза. Команда 3-5 программистов (условный миллион зп в месяц на всех), что могла сделать за год, сделает за 1 неделю. Экономия получается более 11 млн. рублей, казалось бы, да? А заплатить надо, допустим, 1 миллион. Вроде бы надо мгновенно хвататься за такой шанс всеми тремя руками, правда? (и мы даже вопрос недоверия исключим: допустим, есть хороший набор проверенных отзывов от известных компаний, гарантия возврата денег и сохранения всех рабочих процессов as is...).

Ага, щас. CTO CEO будет скрежетать зубами, лишь бы не заплатить даже тыщу долларов за ускорение работы над проектом в сотню раз, и даже "попробовать бесплатно" не сработает. Это ведь в некотором смысле будет признанием своей эээ не совсем полной профессиональной пригодности.

Животные будут с оскаленными клыками охранять свою территорию до последнего:)

Вот есть типичная ситуация с техдолгом "в нашем бэклоге задач на 10 лет вперёд". Вы думаете, тимлид обрадуется предложению "в вашем бэклоге задач на 10 лет вперёд, а через месяц задач останется на один год"?

Да нифига. 98% наёмных менеджеров заинтересованы в максимальном затягивании сроков "по объективным причинам". И даже если удастся договориться с владельцем бизнеса (которые, что (не)удивительно, тоже весьма редко настроены на такие продуктивные изменения, едва дело касается практических телодвижений), на всех остальных уровнях встретится тотальное сопротивление. Потому что и сами разработчики этого совершенно не хотят, для них это просто очередное усиление эксплуатации.

Вот вы начали использовать AI, стали делать тикеты реально во многие разы быстрее, ну и? Выросла ли при этом ваша зарплата хотя бы на 50%? Да хотя бы на 10%?
ФИГ!

"Мы Вы рабы ничего не стоящие, потому что сделали, что должны были сделать"
Лука 17:10

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

Поэтому и коммерческих курсов на эти темы не появится: продавать рост продуктивности даже в сто раз практически нереально. Я общался с PhD из MIT, который вложился в мощные курсы по software design для обычных программистов, но практически никто у него не покупает.

Физики платить в основном готовы за "стать фулстек-программистом с нуля за полгода на 256k" или какие-нибудь быстрые курсы повышения квалификации по техническим фреймворкам, которые постоянно в вакансиях пишутся или востребованы на работе, и всё. А юрики -- за корпоративное обучение чему угодно для галочки (с итоговой нулевой эффективностью), но зато с откатом 98%.

Всё остальное остаётся уделом университетов.

Я вообще один уже наверное остался, кто бредёт в сторону, полностью противоположную мэйнстриму...

Просили пояснить за ТОП: что с этого будет ровным пацанам?

ТОП - это когда мы не просто высокоуровневые спецификации (полученные например с помощью BDD) переводим в некоторый код (как сегодня фактически происходит во всём мировом программировании, от вайб-кодинга с околонуля до монадических механик на этих ваших хаскелях),

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

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

Модульность — через унивалентность (эквивалентность изоморфных структур).
Управление потоком вычислений -- через зависимые типы (как спецификации инвариантов).
Композиция эффектов — через transport along Path (согласованное преобразование контекстов): "переносим" значение из типа A в тип B с сохранением внутренней структуры, если задан путь (доказательство тождества) p : A = B.
Говоря по-программистски, гарантированно безопасное приведение типов.
Сложная логика — через высшие индуктивные типы (инкапсуляция состояний и переходов).

Например, тип List задаёт свободную алгебру над сигнатурой {nil, cons}, а его элиминатор -- рекурсивную схему, логически ограничивая допустимые операции.

Тип (как спецификация пути в ∞-группоиде вычислений) по сути автоматически "выбирает" код своей реализации!

=

Вообще, транспорт через тождества из HoTT (слоистая композиция через когерентные гомотопии, ну или аналог рефакторинга с гарантиями — как вам больше нравится :) -- это прям мощща (монадические bind + pure/return ушли курить далеко и надолго).
Гарантируем, что "побочные эффекты" не нарушают глобальную структуру (на уровне зависимых типов -- например, List -> Vector для конкретной длины).
А сами завтипчики (с продвинутым паттерн-матчингом) позволяют статически кодировать пред- и пост-условия (логика как доказательства), а унивалентность позволяет сменять реализации, сохраняя эквивалентность.

Короче говоря, тип f : (x : A) → B(x) в HoTT -- это не просто функция, а доказательство, что для любого x в A существует конструктивный метод получения B(x), встроенный в целостную гомотопическую структуру типов нашей системы.

Таким образом, подобная система типов становится метаязыком (MetaDSL a-la Math Wins по Алану Кэю) для проектирования логики, где программы -- это не наборы инструкций, а доказательно-топологические конструкции, формально управляемые правилами HoTT.

=

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

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

=

Но мы на курсе это всё конечно разбираем очень-очень просто, без математической терминологии: просто пишем модель гомотопической теории на питончике с очень детальным разбором каждого момента, и понимание темки приходит естественно легко и просто. По сути достаточно лишь PhD это второй-третий курсы хорошего универа, а то и физмат школа (Колмогорова, 1580...).

"К лету курс 💯будет готов."

Предварительный уровень? Ну вот кто прошёл успешно мои курсы "функциональное программирование на F#" и "солвер Z3 на Python", значит готов на 💯

Отчёт за неделю.

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

Апрельские тезисы Алана Кэя, и про первый в мире алгебраический пруф-чекер из 1950-х. Как тебе такое, И.М.?

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

Секретный секрет легендарного миллиардера: как правильное целеполагание забустит вашу продуктивность в космос 🚀 + какую книжечку почитать по теме.

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

СильныеИдеи++
35. Ключевой паттерн Visitor в ООП и ФП
Разбираем примеры Visitor в ООП и ФП, рассматриваем плюсы и минусы каждого, смотрим multiple dispatch, mixins и т.д.

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

Завтра цена подписки для новых донов сильно вырастет.

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

Бусти: закрыт.

Курс "Гомотопическая теория типов для малышей программистов: ТОП (Топологически Ориентированное Программирование)".
"После майских" курс 💯 будет готов. С сегодняшнего дня ре-активирован 🚀
К лету курс 💯будет готов.

Курс "Ясные Системы" (как быстро и легко писать ПРОСТОЙ код систем масштаба ultra-large-scale).
пока 28 эвристик, как наберётся 42, дам курсантам доступ.
Отложен на будущее (которое не настоящее).

Курс "Ясное AI"
"После майских" курс 💯 будет ГОТОВ.

...Далее, полностью сосредотачиваюсь на математике и theoretical computer science. Даже от темок программной инженерии и system design хочу отказаться, и вообще от всего айтишного, где относительно небольшой порог входа — что сегодня может норм пояснить любой ментор с сеньорским опытом или жпт с дипсинком.

В общем, пошёл для начала медитировать, по наводке Алана Кэя, на мета-компилятор Meta II, созданный 60 лет назад для 6-битного компьютера IBM 1401: "A syntax-oriented compiler writing language". Заложенные в него фишечки и по сей день остаются во многом непревзойдёнными и нереализованными.

Его автор Val Schorre придумал крошечную мета-фичу, которая однако сумела сразу охватить семантику широкого спектра языков более высокого уровня ("Math Wins!"). Он также исхитрился применить эту мета-идею к самому мета-компилятору и получить псевдокод для системы, которую смог выполнить простой интерпретатор, запущенный на 1401.

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

Медитирую, соответственно, в мета-направлении "Math Wins!" для современного Software Design, в идеале -- через подобные микро-мета-фишки. Для чего сперва эти мета-фишечки надо смоделировать, в идеале, с помощью гомотопической теории типов. Делаю это всё, конечно, исключительно ДЛЯ ВАС 🙏🙏🙏

❤️ Я буду жить для тебя ❤️

Дорогие, моя Школа ЗАКРЫВАЕТСЯ. Идите с Богом! :)

А я ухожу
в курьеры на постоянку за млн в финтех в стартап AI-онлифанщиц
в математический ретрит.

Больше в платном доступе "для всех" не будет НИ-ЧЕ-ГО.

=

Бусти со вчерашнего дня ЗАКРЫТ, платной подписки больше нету (в мае для последних подписчиков ещё выложу пару материалов).
Пока остаются для покупки сборники материалов СильныхИдей и ещё 2-3 гайда, но цены уже начали расти на ВСЁ.

=

На новой платформе онлайн-обучения со вчерашнего дня также ЗАКРЫТЫ бывшие доступными всем курсы: по TDD, BDD и лямбда-исчислению.

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

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

Билл Гейтс вон решил на неделе все свои 200 млрд. долл. просто раздать на благотоворительность... Я правда, ничего не накопил, но на благотворительность много лет ежемесячно доначу в три фонда: фонд "Старость", фонд Хабенского и WorldVita. Мне даже банк предлагал налоговый вычет за эти донаты (которые я хотел обратно в фонды отправить:), но потом замолк.

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

=

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

Оба паблика VK для донов продолжают работать как обычно!
Сегодня не-начинающим выложил базу про паттерн Visitor -- почему это по сути приляпка, компенсирующая качественные недостатки ООП (данные и поведение хранятся вместе по определению, но наследование может легко поломать LSP), и насколько элегантно проблема решается использованием функционального стиля. 35-й материал, а всего их за сотню будет.

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

Но, стоимость подписки новым донам в обоих пабликах в ближайшие дни РЕЗКО вырастет.

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

На видео: это я в ожидании, когда через 30 минут стартует-Джиро 25 закроется моя Школа.

Я закончил курс "Вайб-проектирование с AI"
(он занял примерно на порядок больше времени чем я предполагал :)

Разбираем тему проектирования при использовании AI. Создаём AI-чат на заданную тему ("персональный мотиватор" с использованием локальной модели или внешнего API) с полного нуля, делая основной акцент на правильном процессе анализа требований и Software/System Design. Практически полностью приведено всё общение с Claude 3.7 и весь код.

Для прохождения курса ничего особенного дополнительно не потребуется,
достаточно локально поставить python + pytorch + transformers + gradio (никаких AI IDE).

Уровень скорее для AI-начинающих -- кто общался с LLM в простом чате, получал от него какие-то кусочки кода и имеет минимальное представление, насколько при таком подходе всё получается печально и как быстро всё запутывается :)
Поэтому на курсе ключевой акцент делаем на Programming in Large.
Ну и для всех тех, кто хочет запустить AI-сервис, но не знает, с чего начать.

22 топика:

БАЗА: Рабочий процесс vibe-кодинга
Рабочий процесс vibe-кодинга: база
1) Мозговой штурм и планирование
2) System Design
2) System Design - 2
2) System Design - 3
Технические шаги
3) Скаффолдинг и спецификации кода
4) Генерация кода в середине цикла
Локальная загрузка модели
Программируем чат с моделью
Генерация генератора промптов
Запускаем сервер
Делаем архитектурную ошибку
Спасаем проэкт
Добавляем внешний API
5) Генерация тестов
6) Два основных приёма отладки с AI
7) Рефакторинг
8) Документация
9) Генерация документов
Итоговый результат

Курс доступен только моим курсантам в рамках трека "Ясные Системы"
(рекомендуется после прохождения курса "Ясное BDD").

картинка от курсанта

P.S. Завтра я сделаю важное заявление о дальнейшем развитии Школы.

С Днём Победы!

Не успел я как следует проснуться, а доставка еды уже заработала! Заказал праздничный стол из kfc. Лифты тоже не тормозили :)

Где-то ближе к 12 прокатился на велике в озон, пункт нормально работает (думаю, по wifi).

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

Ни машин, ни людей на улицах, так классно. Магазины и банкоматы не тестил, но в целом кстати большой ? : если бы мобильный интернет отключился не официально, а наоборот? Почему вдруг в такой ситуации перестают работать приёмы оплаты в магазинах? Конечно, любые кассы должны уметь работать как минимум оффлайн, кэшируя данные (как, собственно, это было всегда). И почему они не переключаются, например, на wifi или проводной интернет? Это же и к банкоматам относится. Они ведь не на улицах стоят, а в тэцэ и всяческих офисных заведениях.

Паникёр: "Сервер упал! Что делать?!"
Айтишник: "Ничего. Он всегда так делает в пятницу в 5 вечера."