Лаборатория Математики и Программирования Сергея Бобровского – Telegram
Лаборатория Математики и Программирования Сергея Бобровского
1.32K subscribers
1.26K photos
27 videos
973 links
ЛаМПовое с Бобровским
Download Telegram
Под конец года подводить итоги важно именно до 25 декабря, потому что завтра нужно уже активировать планы на 2026-й!

Собственно, ключевое достижение -- сделал трек по HoTT/CoC/CTT, и начал стратегический гайд "Функциональные архитектуры", на этих темках и сосредоточусь в следующем году.

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

Ну, сам виноват, потому что нарушил свой же стратегический принцип Лаборатории =>

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

В тему, прочитал на днях, Сергей Брин (третий богач мира) заявил, что уход на пенсию в январе 2020 года был "худшим решением". Так-то он сперва планировал на пенсии "весь день сидеть в кафе и читать книги по физике", но долго не выдержал :) Вернулся в офис Гугла, чтобы поработать с командой Gemini, и теперь говорит, что и технический и творческий результаты были очень полезными."
А так же, что "60-часовая рабочая неделя может стать золотой серединой для повышения продуктивности" :)

Но я о другом: это значит, что обычные люди хотят поскорее уйти на пенсию -- это один полюс, а сверхбогатые/сверхумные люди -- другой полюс -- хотят продолжать много работать и работать.
742🏆1353
Почему программистам платят так много? Мы же буквально просто перемещаем данные из одного места в другое. Это действительно должно быть легко автоматизируемо.
🤔31😁15💯13🐳3🤓2
.

Объявляю 2026-й годом math-стартапов!

Погнали!!1 :)

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

Разработчики почесали репу и решили подстраховаться. Пацаны с гарвардским PhD обобщили этот случай, сформулировали более фундаментальный инвариант, и написали подходящие стратегии для hypothesis (инструмент для автоматического поиска неизвестных ошибок заданного класса; кто им не пользуется, тот лох; а кто не знает, что такое PBT, лох в квадрате).

И действительно, был найден новый, более минимальный контрпример, который не был известен заранее!

Да, но hypothesis работает долго, чтобы найти всего один контрпример. А если нужно проверить все состояния??

Это дорого, это медленно, это малоэффективно, и требует буквально гениев для такой работы.

Вопрос на подумать: можно ли это автоматизировать?

(пауза)

(Кто проходил мой курс по кубической теории типов, в принципе, должен сообразить :)
1👍40🤔8🔥521
.

Как??

Нам надо автоматически вывести нужные стратегии и проперти для условного hypothesis из кода, а затем построить формальное доказательство, а не просто нагенерить тучи случайных тестов.
Автоматизировать труд самых дорогих и редких экспертов в этой темке!
То есть надо автоматически выводить подобные инварианты и контракты из семантики кода, или даже из простой спецификации, + даже обходиться без перебора, применяя символьное "выполнение".

Системы вроде Astree, Coverity, CodeQL, Frama-C -- это по сути просто продвинутые линтеры. Ну, да, Astree умеет даже формально доказывать отсутствие определённых классов ошибок в критическом софте (авиационная/автомобильная промышленность), но весьма ограниченно.

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

(тут мы сваливаемся в Гёделя, проблему полноты, и философские вопросы :)

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

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

В лине например есть Parametric Higher-Order Abstract Syntax, и если мы делегируем связывания его системе типов, то избегаем явной муторщины с de bruijn индексами, и получаем близкую к линейной производительность!
Subterm sharing явно поддерживается на уровне структур данных, и в итоге и rewriting и бета-редукция выполняются за один проход в рамках единой рефлексивной процедуры!! А side conditions при этом проверяем автоматически во время паттерн-матчинга!!!

Выигрыш по времени и по цене? Ну, где-то единицы...десятки тысяч раз. Для Fiat Cryptography например был выигрыш в тысячу, но в чисто академическом эксперименте, и математика там применялась не очень продвинутая.

Резюме: Hypothesis даёт статистическую уверенность, просто некоторую вероятность, механически перебирая мириады случаев. Идея, о которой я рассказал, автоматически доказывает корректность всей процедуры rewriting, приближается к формальной гарантии для всех входных данных. Она не просто найдёт баг в approx_max_k, а сгенерирует доказательство его математической эквивалентности k-топу антропика (или найдёт все условия, когда это не так).
1🤔3587👍2
Чем хорош AI, так это тем, что он даёт каждому уверенность в создании какого-либо программного продукта.

Чем плох AI, так это тем, что он даёт каждому уверенность в создании какого-либо программного продукта.
3😁47💯9🎉8👍53
Что это значит, что практически любой сеньор может перейти на должность тимлида или PM-а, но ни один тимлид/PM не может работать сеньором?
233🤔124👍4💯2
.

В Лаборатории с 29.12.25 по 12.01.26 (вкл) Новогодние/Рождественские каникулы! 🎄
(Но только по явному запросу, так-то по дефолту учебный процесс не прерывается ни на день 💪🏻 )

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

=

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

Приватный клуб.

Алан Кэй отвечает на вопрос, можно ли сегодня спроектировать "self-consistent computational universe", в котором компактная вычислительная мета-модель наподобие языка Forth (минималистичный стековый язык) обеспечит семантическую мощность, аналогичную той, какую в своё время дал Smalltalk для ООП?

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

Синдром самозванца: что ты такое?
Не только начинающие, но и немало сеньоров(!) всё равно думают:
"Это случайность", "Мне просто повезло", "Я всех обманул, и меня скоро разоблачат"...
Всё это порождается из одной базовой мысли ...

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

Как изучить любую тему за 20 часов? Без длительных тренировок и скучных академических подходов?

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

Мы постоянно попадаем в типичную ловушку: люди *знают*, что должны что-то сделать, чтобы заработать больше денег, но не могут заставить себя это сделать. Они считают, что всё решится само собой, если они просто будут терпеливы и просто хорошо поработают.
"В прошлый раз, когда мне предложили работу, я сразу согласился и не стал вести переговоры о зарплате, хотя знал, что должен, и это стоило мне существенной недоплаты".
"Я поговорил с рекрутером и рассказал о своей зарплате, хотя знал, что это не надо делать. Конечно же, их предложение было всего на несколько тысяч выше моей текущей зарплаты".
"Я знал, что должен был проявить инициативу в отношении повышения, но я просто сидел сложа руки и ждал, когда это произойдет само собой. И я всё ещё жду".
Вот как надо: ...

Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим ментатам, но тут расширенные и дополненные версии.
68. Состояние — это время
Если обновление состояния чисто внутреннее, и не может повлиять на наблюдаемое состояние (например, откат транзакции), то оно не ускоряет "программное" время.
Как минимум, это хорошая модель для абстрактных рассуждений о системах. Абстракции — это (почти) всегда про (виртуальное) время! А мы его эксплицитно учитываем крайне редко.

(все старые материалы для донов постепенно сгорают)

=

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

=

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

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

В СильныеИдеи добавлен материал
"131) Микросервисы должны умереть: три архитектурных паттерна на ближайшие годы".
Большинство стартапов умирают не из-за плохого кода. Они умирают из-за неудачных архитектурных решений, которые принимались слишком рано.
Вот неприятная истина, которой мы избегаем:
Вы не можете придумать способ решения проблем, которых у вас ещё нет.


💪🏻

Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.

=

Гайд про функциональные архитектуры, 47 топиков (+7), как наберётся 108, дам ментатам доступ.

Человеческий разум, если его вынудить, может развиваться в обоих направлениях, положительном и отрицательном, в сторону "да" и в сторону "нет". Считайте, что перед вами спектр, пределом которого является бессознательное с одной, отрицательной стороны, и гиперсознание с положительной стороны. И в какую сторону отклонится при воздействии разум, зависит от обучения.
аксиома кодекса Бене Гессерит, "Дюна"
740👍6🔥1
Моя цель в 2026-м году -- достичь целей, которые я поставил в 2025-м году, и которые я должен был сделать в 2024-м году, потому что в 2023-м году я дал обещание, которое запланировал в 2022-м году.

Так-то 2025-й был прекрасным!💥

Скоро сами увидите.
7😁49❤‍🔥1142💯2
Я вот за такой подход 💯 =>

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

пруф

А на практике будет вот так 💯 =>

Делать ХАЙПОВЫЕ игры на Unity, максимально быстро, чаще всего на ассетах и выкладывать их в Гугл, Эппл, Яндекс Игры, Крейзи Геймс и все другие веб площадки, а также на Плейстейшн и Нинтендо.
С Вас: быстрая разработка, желательно на вайб коде, к коду есть только 1 требование, чтоб он работал.
пруф

При том, что британские социобиологи доказали: ИИ превращает людей в дебилов.

А уж в айтишке хард-скиллы растерять через "помощь" AI совершенно реально, буквально за считанные месяцы.
2💯44🤔84
Ни один талантливый программист не использует макбуки.

Только (arch) linux.
😁4616👌6💯32
Представьте, что будет с вашей карьерой в 2026-м году, если вы действительно сделаете то, о чём сегодня говорите, и что будете планировать на год в ближайшие дни! 🚀
355🏆13
Ну, с Наступившим и вот это всё... Салатиками подкрепились?
Пора браться за кодинг!1

Часто вы думаете, что усердно работаете, пока не увидите кого-то, кто на самом деле усердно работает 💪🏻
942💯15🎉6🏆5🫡4
Хочу вам сказать, что по-настоящему трудолюбивый человек не чувствует необходимости рассказывать другим, как усердно он работает.
3👍43💯238😁6🤔1
cейчас самое время сломать Систему =>
удержать себя от бухания и пережирания =>
ну и так-то Рождественский Пост, напомню =>
заняться сложной интеллектуальной деятельностью!

и я начал на новогодних делать клон dwarf fortress

и наконец-то разобрался с асинхронной ошибкой,
ибо моделируем сложнейший мир в реалтайме

я буквально лучший!

лучше меня в программировании нет никого!!

я гений!!1

...блин, через ~12 минут снова застрял
6😁54🔥14❤‍🔥7🐳4🏆3
не могу найти ошибку в течение 3 часов.
выхожу на 10-минутную прогулку.
обнаруживаю ошибку за 2 минуты.

асинхронная отладка - это буквально просто добавление логов.
print("Fuck!")

Работать нужно уже со 2 января, иначе праздники станут мучением. Схема идеального Нового года простая: 30 декабря уйти пораньше, 31 отметить, 1 января выспаться -- и уже 2-го бодро включиться в рабочие задачи.
академик Геннадий Онищенко
145💯199👌5
Если периодически заглядывать под капот клауд кода и смотреть, а какой вообще код пишут жпт агенты, то регулярно будешь видеть вот такое ↑↑↑
😁56🤔53
В декабре 2025-го вышли две классные книги - почти одновременно!
- в крайне важной стратегически, но крайне сложной темке!
- причём на русском! что (особенно по нынешним временам) событие абсолютно удивительное, впервые лет за 5-10, а может быть и больше.

Сразу взял обе книги, очень рекомендую кто занимается на второй части Лаборатории.

1. "Проектирование на уровне типов"
Александр Гранин (известный эксперт в ФП и Хаскеле, в 2025-м выпустил книгу "Functional Design and Architecture", работает в Европе уже давно).
Блог Александра.

2. "Аксиоматическая архитектура научных теорий" (переработанная докторская)
Андрей Родин (последний русский HoTT-математик, уехал во Францию в 2023-м).

Последовательное введение в, по сути, формализацию математики для всех интересующихся темой: "От Евклида до Гильберта => Гомотопическая теория типов и унивалентные основания математики".

Европейская школа в этой нише, да и в computer science в целом, на сегодня абсолютный топчик (недавно и наша школа была с ней на одном уровне, а теперь в России физически из неё я наверное остался один, да и то непонятно, насколько долго :).

Ссылки на бумажные и электронные книги ищите по ссылкам выше.

В гайд "Функциональные архитектуры" понемногу готовлю и из них выжимки)))

А для разогрева можно насладиться классным стримом Мокевнина и Вершилова про Haskell.
54817😁4
Российский ИТ-бизнес в 2026-м: мой пост в Максе и Рутубе, набравший более 42 000 000 показов, привлёк 18 новых платных (150 рублей/месяц) пользователей к моему SaaS-продукту!!1
😁48🔥146👍1
Конечно, искусственный интеллект сегодня позволяет программистам быстрее (и тупо, без малейшего понимания) копировать топовых элитных разработчиков, но здесь есть и хорошие новости:

Большинство людей просто ничего не делают.

Вот как ты сейчас :)

На самом деле до смешного легко превзойти большинство людей в айтишной карьере: средний человек невероятно ленив.
232💯23🔥11🤔62
.

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

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

Собственно, и сам жпт это определяет норм:
вот для решения, где я вижу, что честно делалось =>
"вероятность, что этот код писала нейросеть, в диапазоне 10–25%."
и где явный нейрослоп =>
"На основе анализа кода я оцениваю вероятность того, что он написан нейросетью, в диапазоне 65–85%."

Ну и как бы даже странно обсуждать, почему. Человек платит деньги, чтобы ничему не учиться? Ну так я не держу, всё равно у меня везде пост-оплата, просто брось занятия и всё. Где логика, где разум? :)

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

Приватный клуб.

null

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

null

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

Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим ментатам, но тут расширенные и дополненные версии.
69. О пользе формальных спецификаций
Когда здесь остановиться? Как вообще правильно думать о соотношении абстрактной спецификации Abstract с нашей реализацией Impl?

(все старые материалы для донов постепенно сгорают)

=

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

=

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

В курс карьеры добавлен 123-й материал "Почему одни растут быстрее других?".
Привожу типичный шаблон - обобщение опыта многих десятков сеньоров, которые росли по карьере существенно быстрее других. Как? Отличительная особенность этого шаблона в том, что он в значительной степени контринтуитивен, и его не найти ни в статьях, ни в нейросетях...

"ЛаМПовое": ассемблер олдскул, strcpy слоп

💪🏻

Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.

=

Гайд про функциональные архитектуры, 47 топиков (+0), как наберётся 108, дам ментатам доступ.

Ментат продвигается вперёд как римлянин, управляющий колесницей — ноги стоят на разных конях упряжки. Каждая нога покоится на отличной от другой реальности, но поиск смыслового рисунка побуждает ментата двигаться вперёд. Он скачет к смыслу на разных реальностях, чтобы достичь единой цели.
"Еретики Дюны"
1🔥30🏆106🫡5👍2
Продолжаю работу с ментатами 🤓

...За этот год написал в тг-канал 75 постов. Большую часть во второй половине года. Кол-во подписчиков перевалило за 100 и постепенно растет. Некоторые посты даже репостят (16 раз), чему я был удивлен. Активность подписчиков (в основном это разработчики) придает уверенности в себе. Мне пишут в комментариях, делятся опытом, спрашивают совет. Круг общения однозначно расширился.
Хочу дальше развиваться в этом направлении. Я впервые в этом году смог почувствовать пользу от ведения блога в виде новых знаний, контактов, предложений работы и просто приятного общения.

...В этом году мой вклад в большое количество работы окупился в виде премии - получилось около +100к к ежемесячной зарплате.

...Откликался на вакансии hh. В данный момент откликнулся на 21 вакансию из которых получил отказ 3 раза и 4 ответа с просьбой заполнить анкету или сделать тестовое задание, остальные непросмотрены... Для одной вакансии дали тестовое задание - отправил, позвали на собеседование в понедельник. Отправлял в откликах заказанное резюме - это отличный совет, сам бы так не написал.

...Первая значимая (хоть и промежуточная) веха на пути к цели – завел профиль на hh и опубликовал в открытый доступ первый «драфт» резюме. Резюме пока сильно на «троечку», но тут как раз уже стимул оперативно его доработать согласно всему изученному по видео и материалам КК. В самых ближайших планах по hh – дооформить раздел «обо мне», подтвердить пару-тройку основных навыков и доредактировать само резюме конечно же. Далее уже буду переходить к профилю в LinkedIn.
Неделю назад в анонсе материала по математике высокой продуктивности от одного из ментатов было упоминание материала 48 из ЭП – не удержался и, т.к. пока все равно не вернулся на последовательное изучение трека, прочитал его :) И однозначно не пожалел. На самом деле я интуитивно этот подход уже использовал, но т.к. в голове он не был формализован, очень нерегулярно и непоследовательно применялся. И вот как раз для текущего последнего задания по диплому по микросервисам этот подход максимально подошел – уже сознательно примененный.

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

...Досрочно завершил испытательный, пару недель вместо месяца, сказали результат показал
Испытательный оплатят, поскольку мое поделие пойдет в прод
Часовую ставку назначили больше, чем у меня сейчас на руководящей должности в крупной компании
Ещё раз спасибо за Ваш труд, чем дальше я иду, тем больше удивляюсь масштабу проведенной Вами в Школе работы!

...А ещё вроде РТК ИТ кого-то выкупил и возможно в следующем году пул задач расширится и понадобятся новые люди.

...Дело в том что у меня, насколько понимаю, заработал интернет по белым спискам. Нет доступа ни к github ни к каким другим сайтам особо. VPN которые прежде использовал не помогают.

...Был на техническом собесдовании в Яндекс. Переволновался и забыл откуда импортируется мок объект, пришлось в моменте создавать класс мок, который имитироваля внешние api. После сдачи задачи проверил код - было 3 бага на 70 строк.

Вот ровно поэтому надо постоянно тренироваться в интервью с живым людьми, и моки и реальные, сколько лет я об этом пишу...


Получил первую повышенную зарплату полностью на руки :)
Цель достигнута.
Самое главное понял для себя, что повышение оклада – это не какая-то разовая активность, а перманентный процесс повышения своей ценности, который основывается непосредственно на профессиональном росте как в хардах, так и в развитии софт-скиллов. Вообще, дико банальная фраза получилась, и не то, чтобы я это как-то совсем не понимал раньше, но при целенаправленной работе в данном направлении эта зависимость чувствуется как-то более явно что ли :)
1👍41111