Дэвид Бадден, экс-глава Deep Learning в DeepMind, грозится решить проблему Навье-Стокса (одна из семи математических задач тысячелетия, база гидродинамики) ещё в этом году.
Он выложил предварительный код формального доказательства на Lean4 (из России топовые математики без винни-пуха недоступны), и забился на 10k баксов с профессором Маркусом Хаттером (автор AIXI, теоретической модели универсального агента).
Но сам приз так-то миллион долларов, ставки делают, правда 98% не верят что получится, и я тоже:)
Но хайпанул пацан чётко. не ну а чо.
А я только три дня назад эту идею спалил =>
"Идея для math-стартапа: перевОдите это (и другие подобные от топовых математиков) доказательство в формальный вид на теорем-прувере вроде Lean или Coq, и получаете реальную мировую известность."
Дэвид, раз читаешь мой блог, задонать сотку баксов :)
Он выложил предварительный код формального доказательства на Lean4 (из России топовые математики без винни-пуха недоступны), и забился на 10k баксов с профессором Маркусом Хаттером (автор AIXI, теоретической модели универсального агента).
Но сам приз так-то миллион долларов, ставки делают, правда 98% не верят что получится, и я тоже:)
Но хайпанул пацан чётко. не ну а чо.
THE PROOF IS COMPLETE.
All logical steps are formalized. The theorem `navier_stokes_regularity` proves:
For any NS solution satisfying the physical axioms, blowup is impossible.
The physical axioms are:
1. Type II exponent α > 1 (from ESS theorem)
2. Spectral gap νP ≥ c•Ω•E (from Poincaré on dissipation scale)
3. θ dynamics S ≤ C•(T-t)^{α-1}•Ω•E (from alignment ODE)
4. Blowup rate Ω ≤ C•(T-t)^{-α} (from Type II characterization)
5. BKM criterion (from Agmon interpolation)
Each axiom is verified from NS physics in the accompanying theorems.
А я только три дня назад эту идею спалил =>
"Идея для math-стартапа: перевОдите это (и другие подобные от топовых математиков) доказательство в формальный вид на теорем-прувере вроде Lean или Coq, и получаете реальную мировую известность."
Дэвид, раз читаешь мой блог, задонать сотку баксов :)
X (formerly Twitter)
Budden (@davidmbudden) on X
https://t.co/bmTXoAESgD
7🔥42😁10👍4
Под конец года подводить итоги важно именно до 25 декабря, потому что завтра нужно уже активировать планы на 2026-й!
Собственно, ключевое достижение -- сделал трек по HoTT/CoC/CTT, и начал стратегический гайд "Функциональные архитектуры", на этих темках и сосредоточусь в следующем году.
Эпикфейл года: зачем-то связался со сторонним сервисом онлайн-курсов, сделал на нём семь небольших, а под конец года этот сервис внезапно выкатил требование регистрируйтесь как операторы перс.данных иначе штраф 400т. А там возни дохренища на пустом месте по сути. В итоге слил кучу денег и, главное, времени.
Ну, сам виноват, потому что нарушил свой же стратегический принцип Лаборатории =>
"Никогда не буду брать в помощь кого-то ещё, или заключать с кем-то соглашения о партнёрстве (абсолютно всё, от текстовых курсов до программирования учебных сервисов, делаю в одиночку)."
В тему, прочитал на днях, Сергей Брин (третий богач мира) заявил, что уход на пенсию в январе 2020 года был "худшим решением". Так-то он сперва планировал на пенсии "весь день сидеть в кафе и читать книги по физике", но долго не выдержал :) Вернулся в офис Гугла, чтобы поработать с командой Gemini, и теперь говорит, что и технический и творческий результаты были очень полезными."
А так же, что "60-часовая рабочая неделя может стать золотой серединой для повышения продуктивности" :)
Но я о другом: это значит, что обычные люди хотят поскорее уйти на пенсию -- это один полюс, а сверхбогатые/сверхумные люди -- другой полюс -- хотят продолжать много работать и работать.
Собственно, ключевое достижение -- сделал трек по HoTT/CoC/CTT, и начал стратегический гайд "Функциональные архитектуры", на этих темках и сосредоточусь в следующем году.
Эпикфейл года: зачем-то связался со сторонним сервисом онлайн-курсов, сделал на нём семь небольших, а под конец года этот сервис внезапно выкатил требование регистрируйтесь как операторы перс.данных иначе штраф 400т. А там возни дохренища на пустом месте по сути. В итоге слил кучу денег и, главное, времени.
Ну, сам виноват, потому что нарушил свой же стратегический принцип Лаборатории =>
"Никогда не буду брать в помощь кого-то ещё, или заключать с кем-то соглашения о партнёрстве (абсолютно всё, от текстовых курсов до программирования учебных сервисов, делаю в одиночку)."
В тему, прочитал на днях, Сергей Брин (третий богач мира) заявил, что уход на пенсию в январе 2020 года был "худшим решением". Так-то он сперва планировал на пенсии "весь день сидеть в кафе и читать книги по физике", но долго не выдержал :) Вернулся в офис Гугла, чтобы поработать с командой Gemini, и теперь говорит, что и технический и творческий результаты были очень полезными."
А так же, что "60-часовая рабочая неделя может стать золотой серединой для повышения продуктивности" :)
Но я о другом: это значит, что обычные люди хотят поскорее уйти на пенсию -- это один полюс, а сверхбогатые/сверхумные люди -- другой полюс -- хотят продолжать много работать и работать.
7❤42🏆13✍5⚡3
.
Объявляю 2026-й годом math-стартапов!
Погнали!!1 :)
У Антропика есть такой известный баг, когда в Клоде сбрасывается наиболее вероятный токен из-за того, что не удаётся корректно согласовать вычисления на разных TPU из-за дефолтных настроек оптимизирующего векторного компилятора XLA
(а надо было изучать мои гайды по параллельным вычислительным моделям:). Баг и сегодня легко воспроизводится десятком строк кода на питоне.
Ну, а то что миллионы пользователей периодически получали явно ошибочные решения, никого особо не волнует.
Разработчики почесали репу и решили подстраховаться. Пацаны с гарвардским PhD обобщили этот случай, сформулировали более фундаментальный инвариант, и написали подходящие стратегии для hypothesis(инструмент для автоматического поиска неизвестных ошибок заданного класса; кто им не пользуется, тот лох; а кто не знает, что такое PBT, лох в квадрате) .
И действительно, был найден новый, более минимальный контрпример, который не был известен заранее!
Да, но hypothesis работает долго, чтобы найти всего один контрпример. А если нужно проверить все состояния??
Это дорого, это медленно, это малоэффективно, и требует буквально гениев для такой работы.
Вопрос на подумать: можно ли это автоматизировать?
(пауза)
(Кто проходил мой курс по кубической теории типов, в принципе, должен сообразить :)
Объявляю 2026-й годом math-стартапов!
Погнали!!1 :)
У Антропика есть такой известный баг, когда в Клоде сбрасывается наиболее вероятный токен из-за того, что не удаётся корректно согласовать вычисления на разных TPU из-за дефолтных настроек оптимизирующего векторного компилятора XLA
(а надо было изучать мои гайды по параллельным вычислительным моделям:). Баг и сегодня легко воспроизводится десятком строк кода на питоне.
Ну, а то что миллионы пользователей периодически получали явно ошибочные решения, никого особо не волнует.
Разработчики почесали репу и решили подстраховаться. Пацаны с гарвардским PhD обобщили этот случай, сформулировали более фундаментальный инвариант, и написали подходящие стратегии для hypothesis
И действительно, был найден новый, более минимальный контрпример, который не был известен заранее!
Да, но hypothesis работает долго, чтобы найти всего один контрпример. А если нужно проверить все состояния??
Это дорого, это медленно, это малоэффективно, и требует буквально гениев для такой работы.
Вопрос на подумать: можно ли это автоматизировать?
(пауза)
(Кто проходил мой курс по кубической теории типов, в принципе, должен сообразить :)
1👍40🤔8🔥5❤2✍1
.
Как??
Нам надо автоматически вывести нужные стратегии и проперти для условного 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-топу антропика (или найдёт все условия, когда это не так).
Как??
Нам надо автоматически вывести нужные стратегии и проперти для условного 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🤔35❤8✍7👍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, дам ментатам доступ.
Человеческий разум, если его вынудить, может развиваться в обоих направлениях, положительном и отрицательном, в сторону "да" и в сторону "нет". Считайте, что перед вами спектр, пределом которого является бессознательное с одной, отрицательной стороны, и гиперсознание с положительной стороны. И в какую сторону отклонится при воздействии разум, зависит от обучения.
аксиома кодекса Бене Гессерит, "Дюна"
В Лаборатории с 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, дам ментатам доступ.
Человеческий разум, если его вынудить, может развиваться в обоих направлениях, положительном и отрицательном, в сторону "да" и в сторону "нет". Считайте, что перед вами спектр, пределом которого является бессознательное с одной, отрицательной стороны, и гиперсознание с положительной стороны. И в какую сторону отклонится при воздействии разум, зависит от обучения.
аксиома кодекса Бене Гессерит, "Дюна"
7❤40👍6🔥1
Я вот за такой подход 💯 =>
Мой главный вывод: ИИ оказался ужасно переоценен. Уже несколько лет студии разного пошиба прочно интегрируют ИИ в процесс разработки, однако результаты ничего толком не поменяли: разработка игр не подешевела (почему-то); само качество популярных проектов не изменилось и они не стали выходить в разы чаще. Игроки регулярно проявляют открытую ненависть к ИИ в играх. Разработчики с головой на плечах очень осторожничают в этом вопросе: им остается или не использовать ИИ вовсе, или максимально его маскировать, что только замедляет процесс разработки.
пруф
А на практике будет вот так 💯 =>
Делать ХАЙПОВЫЕ игры на Unity, максимально быстро, чаще всего на ассетах и выкладывать их в Гугл, Эппл, Яндекс Игры, Крейзи Геймс и все другие веб площадки, а также на Плейстейшн и Нинтендо.
С Вас: быстрая разработка, желательно на вайб коде, к коду есть только 1 требование, чтоб он работал.
пруф
При том, что британские социобиологи доказали: ИИ превращает людей в дебилов.
А уж в айтишке хард-скиллы растерять через "помощь" AI совершенно реально, буквально за считанные месяцы.
Мой главный вывод: ИИ оказался ужасно переоценен. Уже несколько лет студии разного пошиба прочно интегрируют ИИ в процесс разработки, однако результаты ничего толком не поменяли: разработка игр не подешевела (почему-то); само качество популярных проектов не изменилось и они не стали выходить в разы чаще. Игроки регулярно проявляют открытую ненависть к ИИ в играх. Разработчики с головой на плечах очень осторожничают в этом вопросе: им остается или не использовать ИИ вовсе, или максимально его маскировать, что только замедляет процесс разработки.
пруф
А на практике будет вот так 💯 =>
Делать ХАЙПОВЫЕ игры на Unity, максимально быстро, чаще всего на ассетах и выкладывать их в Гугл, Эппл, Яндекс Игры, Крейзи Геймс и все другие веб площадки, а также на Плейстейшн и Нинтендо.
С Вас: быстрая разработка, желательно на вайб коде, к коду есть только 1 требование, чтоб он работал.
пруф
При том, что британские социобиологи доказали: ИИ превращает людей в дебилов.
А уж в айтишке хард-скиллы растерять через "помощь" AI совершенно реально, буквально за считанные месяцы.
2💯44🤔8❤4
Хочу вам сказать, что по-настоящему трудолюбивый человек не чувствует необходимости рассказывать другим, как усердно он работает.
3👍43💯23❤8😁6🤔1
cейчас самое время сломать Систему =>
удержать себя от бухания и пережирания =>
ну и так-то Рождественский Пост, напомню =>
заняться сложной интеллектуальной деятельностью!
и я начал на новогодних делать клон dwarf fortress
и наконец-то разобрался с асинхронной ошибкой,
ибо моделируем сложнейший мир в реалтайме
я буквально лучший!
лучше меня в программировании нет никого!!
я гений!!1
...блин, через ~12 минут снова застрял
удержать себя от бухания и пережирания =>
ну и так-то Рождественский Пост, напомню =>
заняться сложной интеллектуальной деятельностью!
и я начал на новогодних делать клон dwarf fortress
и наконец-то разобрался с асинхронной ошибкой,
ибо моделируем сложнейший мир в реалтайме
я буквально лучший!
лучше меня в программировании нет никого!!
я гений!!1
6😁54🔥14❤🔥7🐳4🏆3
не могу найти ошибку в течение 3 часов.
выхожу на 10-минутную прогулку.
обнаруживаю ошибку за 2 минуты.
асинхронная отладка - это буквально просто добавление логов.
Работать нужно уже со 2 января, иначе праздники станут мучением. Схема идеального Нового года простая: 30 декабря уйти пораньше, 31 отметить, 1 января выспаться -- и уже 2-го бодро включиться в рабочие задачи.
академик Геннадий Онищенко
выхожу на 10-минутную прогулку.
обнаруживаю ошибку за 2 минуты.
асинхронная отладка - это буквально просто добавление логов.
print("Fuck!")Работать нужно уже со 2 января, иначе праздники станут мучением. Схема идеального Нового года простая: 30 декабря уйти пораньше, 31 отметить, 1 января выспаться -- и уже 2-го бодро включиться в рабочие задачи.
академик Геннадий Онищенко
1❤45💯19✍9👌5
В декабре 2025-го вышли две классные книги - почти одновременно!
- в крайне важной стратегически, но крайне сложной темке!
- причём на русском! что (особенно по нынешним временам) событие абсолютно удивительное, впервые лет за 5-10, а может быть и больше.
Сразу взял обе книги, очень рекомендую кто занимается на второй части Лаборатории.
1. "Проектирование на уровне типов"
Александр Гранин (известный эксперт в ФП и Хаскеле, в 2025-м выпустил книгу "Functional Design and Architecture", работает в Европе уже давно).
Блог Александра.
2. "Аксиоматическая архитектура научных теорий" (переработанная докторская)
Андрей Родин (последний русский HoTT-математик, уехал во Францию в 2023-м).
Последовательное введение в, по сути, формализацию математики для всех интересующихся темой: "От Евклида до Гильберта => Гомотопическая теория типов и унивалентные основания математики".
Европейская школа в этой нише, да и в computer science в целом, на сегодня абсолютный топчик (недавно и наша школа была с ней на одном уровне, а теперь в России физически из неё я наверное остался один, да и то непонятно, насколько долго :).
Ссылки на бумажные и электронные книги ищите по ссылкам выше.
В гайд "Функциональные архитектуры" понемногу готовлю и из них выжимки)))
А для разогрева можно насладиться классным стримом Мокевнина и Вершилова про Haskell.
- в крайне важной стратегически, но крайне сложной темке!
- причём на русском! что (особенно по нынешним временам) событие абсолютно удивительное, впервые лет за 5-10, а может быть и больше.
Сразу взял обе книги, очень рекомендую кто занимается на второй части Лаборатории.
1. "Проектирование на уровне типов"
Александр Гранин (известный эксперт в ФП и Хаскеле, в 2025-м выпустил книгу "Functional Design and Architecture", работает в Европе уже давно).
Блог Александра.
2. "Аксиоматическая архитектура научных теорий" (переработанная докторская)
Андрей Родин (последний русский HoTT-математик, уехал во Францию в 2023-м).
Последовательное введение в, по сути, формализацию математики для всех интересующихся темой: "От Евклида до Гильберта => Гомотопическая теория типов и унивалентные основания математики".
Европейская школа в этой нише, да и в computer science в целом, на сегодня абсолютный топчик (недавно и наша школа была с ней на одном уровне, а теперь в России физически из неё я наверное остался один, да и то непонятно, насколько долго :).
Ссылки на бумажные и электронные книги ищите по ссылкам выше.
В гайд "Функциональные архитектуры" понемногу готовлю и из них выжимки)))
А для разогрева можно насладиться классным стримом Мокевнина и Вершилова про Haskell.
5✍48❤17😁4
Конечно, искусственный интеллект сегодня позволяет программистам быстрее (и тупо, без малейшего понимания) копировать топовых элитных разработчиков, но здесь есть и хорошие новости:
Большинство людей просто ничего не делают.
Вот как ты сейчас :)
На самом деле до смешного легко превзойти большинство людей в айтишной карьере: средний человек невероятно ленив.
Большинство людей просто ничего не делают.
На самом деле до смешного легко превзойти большинство людей в айтишной карьере: средний человек невероятно ленив.
2⚡32💯23🔥11🤔6❤2
.
Облако драгоценностей за неделю.
Важное правило занятий 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, дам ментатам доступ.
Ментат продвигается вперёд как римлянин, управляющий колесницей — ноги стоят на разных конях упряжки. Каждая нога покоится на отличной от другой реальности, но поиск смыслового рисунка побуждает ментата двигаться вперёд. Он скачет к смыслу на разных реальностях, чтобы достичь единой цели.
"Еретики Дюны"
Облако драгоценностей за неделю.
Важное правило занятий 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🏆10❤6🫡5👍2