В штаб-квартире Национальной службы информационных ресурсов NIRS Южной Кореи произошёл пожар, в результате которого были уничтожены файлы, хранившие данные по 750 000 госслужащих за последние семь лет.
Резервные копии "технически" у них были, но они также оказались уничтожены 🙈 в результате того же пожара 🔥
Вы же знаете базу 3-2-1 ? ваша стратегия резервного копирования должна предусматривать 3 копии: на 2 физически разных типа носителя в разнесённых помещениях + 1 удалённую копию. А я бы вообще хранил две удалённые: одну в чужом облаке, а другую на флешке на даче.
Резервные копии "технически" у них были, но они также оказались уничтожены 🙈 в результате того же пожара 🔥
Вы же знаете базу 3-2-1 ? ваша стратегия резервного копирования должна предусматривать 3 копии: на 2 физически разных типа носителя в разнесённых помещениях + 1 удалённую копию. А я бы вообще хранил две удалённые: одну в чужом облаке, а другую на флешке на даче.
🤯35💯15❤7😁5👌2
База от нашего ментата =>
1. Понял, что резюме — это пропуск на первый этап. Буду адаптировать его под конкретные вакансии: вставлять нужные ключевые слова и подсвечивать релевантные навыки.
2. Запомнил важную мысль: с рекрутерами нужно говорить простым языком. Никакого "рефакторинга" и "микрофронтов" — им важно понять меня как человека, а не погружаться в технические дебри.
3. Веду детальную таблицу со всеми откликами, результатами и фидбеком. Это помогает видеть картину целиком и понимать, что работает.
4. Записываю все интервью и скрининги. Без разбора полетов буду наступать на одни и те же грабли.
5. Понял, что подход должен меняться: с HR показываю опыт, на техническом — демонстрирую навыки, с будущим руководителем — фокусируюсь на софт скиллах и совместимости.
6. Буду учиться мыслить категориями бизнеса и понимать, как моя работа влияет на результаты компании. Это поможет говорить с командой на одном языке и правильно расставлять приоритеты.
7. Активно задаю вопросы о проекте, технологиях, команде. Превращаю собеседование в живое общение, а не односторонний опрос.
8. Не игнорирую небольшие компании — у них выше шансы получить приглашение, чем в крупных IT-гигантах типа Яндекса или Сбера.
А чего добился ты? Можешь вот так структурировать свой подход?
1. Понял, что резюме — это пропуск на первый этап. Буду адаптировать его под конкретные вакансии: вставлять нужные ключевые слова и подсвечивать релевантные навыки.
2. Запомнил важную мысль: с рекрутерами нужно говорить простым языком. Никакого "рефакторинга" и "микрофронтов" — им важно понять меня как человека, а не погружаться в технические дебри.
3. Веду детальную таблицу со всеми откликами, результатами и фидбеком. Это помогает видеть картину целиком и понимать, что работает.
4. Записываю все интервью и скрининги. Без разбора полетов буду наступать на одни и те же грабли.
5. Понял, что подход должен меняться: с HR показываю опыт, на техническом — демонстрирую навыки, с будущим руководителем — фокусируюсь на софт скиллах и совместимости.
6. Буду учиться мыслить категориями бизнеса и понимать, как моя работа влияет на результаты компании. Это поможет говорить с командой на одном языке и правильно расставлять приоритеты.
7. Активно задаю вопросы о проекте, технологиях, команде. Превращаю собеседование в живое общение, а не односторонний опрос.
8. Не игнорирую небольшие компании — у них выше шансы получить приглашение, чем в крупных IT-гигантах типа Яндекса или Сбера.
А чего добился ты? Можешь вот так структурировать свой подход?
❤46👍15✍7🐳3❤🔥1
Рефакторинг -- это трансформация унаследованного (по определению) кода без изменения его функциональности.
Если посмотреть на такую трансформацию через линзу HoTT, то это будет, по сути, умение видеть (понимание) эквивалентности между различными парадигмами полиморфизма.
1. Параметрический полиморфизм -- это база универсальности.
Функция
работает единообразно для любых типов a и b. Нам не нужно (да и невозможно) "заглядывать" внутрь a.
Это гомотопия (непрерывное преобразование), гомотопическая инвариантность.
Тип
Такая программа будет постоянной на эквивалентных типах: она не может делать странных вещей, зависящих от конкретного типа (для строк -- удваивать, а для чисел -- извлекать корень), из чего гарантируется её универсальность.
Параметрический полиморфизм -- это "контракт", который гарантирует, что полиморфная функция универсальна.
Если посмотреть на такую трансформацию через линзу HoTT, то это будет, по сути, умение видеть (понимание) эквивалентности между различными парадигмами полиморфизма.
1. Параметрический полиморфизм -- это база универсальности.
Функция
map (f: 'a -> 'b) (list: 'a list) : 'b listработает единообразно для любых типов a и b. Нам не нужно (да и невозможно) "заглядывать" внутрь a.
Это гомотопия (непрерывное преобразование), гомотопическая инвариантность.
Тип
forall a b. (a -> b) -> List a -> List b -- это пространство всех возможных реализаций (всех функций с данным типом, и все они гомотопически эквивалентны).Такая программа будет постоянной на эквивалентных типах: она не может делать странных вещей, зависящих от конкретного типа (для строк -- удваивать, а для чисел -- извлекать корень), из чего гарантируется её универсальность.
Параметрический полиморфизм -- это "контракт", который гарантирует, что полиморфная функция универсальна.
❤37🤔19👍4❤🔥1
1. Параметрический полиморфизм -- это база универсальности.
2. ad-hoc полиморфизм -- это зависимые типы.
Программист работает с интерфейсами или перегрузкой функций (трейты, тайпклассы...). Функция
ведет себя по-разному для Int, Float и т.д.
К сожалению, на F# так компактно как в хаске записать подобную сигнатуру невозможно :(
Нужен when constraint с ^T, +, Zero...
Ладно, вот вам жава, для наглядности )
Так вот, это по сути работа с зависимыми типами. Ограничение
Тип Num a -- это тип-пропозиция, которая может быть либо доказана (и тогда мы получаем конкретную реализацию), либо нет. Таким образом, выбор реализации -- это просто применение функции к нужному "пруфу".
На практике имеем гарантии на этапе компиляции, явные контракты (сигнатура функции явно говорит о требованиях), и нужное нам для рефакторинга безопасное расширение функциональности. Не совсем завтипчики, но дух уже чувствуется )
Кто проходил мой курс по F#, попробуйте дописать до полноценного примера.
2. ad-hoc полиморфизм -- это зависимые типы.
Программист работает с интерфейсами или перегрузкой функций (трейты, тайпклассы...). Функция
sum : Num a => [a] -> aведет себя по-разному для Int, Float и т.д.
К сожалению, на F# так компактно как в хаске записать подобную сигнатуру невозможно :(
Нужен when constraint с ^T, +, Zero...
Ладно, вот вам жава, для наглядности )
public int sum(List<Integer> list)
public double sum(List<Double> list)
Так вот, это по сути работа с зависимыми типами. Ограничение
Num a (Integer list, Double list) -- это не просто помощь компилятору/тайпчекеру, а дополнительный аргумент, который функция sum неявно принимает. Этот аргумент -- доказательство того, что для типа a существует реализация интерфейса Num. Тип Num a -- это тип-пропозиция, которая может быть либо доказана (и тогда мы получаем конкретную реализацию), либо нет. Таким образом, выбор реализации -- это просто применение функции к нужному "пруфу".
На практике имеем гарантии на этапе компиляции, явные контракты (сигнатура функции явно говорит о требованиях), и нужное нам для рефакторинга безопасное расширение функциональности. Не совсем завтипчики, но дух уже чувствуется )
type Money = { Amount: decimal; Currency: string }
// пруф 1: сложение только одинаковых валют
let sameCurrencyAdd a b = ...
// пруф 2: сложение с конвертацией по курсу
let convertAndAdd (exchangeRate: string -> string -> decimal) a b = ...
let money1 = { Amount = 100m; Currency = "USD" }
let money2 = { Amount = 500m; Currency = "RUB" }
sum convertAndAdd ... [money1; money2] - сконвертирует и сложит
sum sameCurrencyAdd ... [money1; money2] - ошибка компиляцииКто проходил мой курс по F#, попробуйте дописать до полноценного примера.
❤37✍12👍2
1. Параметрический полиморфизм -- это база универсальности.
2. ad-hoc полиморфизм -- это зависимые типы.
3. Сабтайпинг ("наследование") -- это эквивалентность.
Circle -- подтип Shape. Везде, где ожидается Shape, можно использовать Circle.
Профит! )))
(На самом деле, тут немеряное количество засад даже на уровне базы SOLID, особенно по LSP; всё это подробно, с анализом в ФП, разбирал в большом гайде)
По-взрослому же, в HoTT используется эквивалентность типов и унивалентность. Если тип Circle можно преобразовать в тип Shape, то это преобразование считается "путём" между типами. А унивалентность гарантирует, что если такой путь существует, то он по сути и есть "правильное" "наследование". Другими словами, любое свойство, доказанное для всех Shape, автоматически выполняется и для Circle (потому что с точки зрения логики предикатов они находятся в отношении эквивалентности).
Классическое наследование -- это частный случай построения такого "пути-функции" из подтипа в супертип.
При этом мы получаем все "инженерные" фишки ООП (SOLID и Co) "в коробке", за нас всё делает HoTT-"движок". Например, в Shape есть area() (вычисление площади), которая всегда должна быть положительной. Но в реализации Circle она может быть нулевой, и тем самым мы нарушаем LSP.
В HoTT же "нарушить LSP" технически невозможно: система типов (топовая в мире на сегодня) гарантирует, что все случаи обработаны корректно. Подтипизация тут моделируется через эквивалентность, которая сохраняет все свойства: если какой-то подтип не удовлетворяет всем свойствам супертипа, то мы просто не сможем доказать эти свойства для супертипа, и значит, не сможем применить их к подтипу.
Другими словами, при нарушении LSP (и многих других солид-шмолид etc) мы получим ошибку компиляции.
=
Другое дело, что сегодня таких "языков программирования", реализующих HoTT (или хотя бы просто завтипы), которые можно было бы считать массовыми хотя бы на 2%, нету и особо не ожидается (в первую очередь потому, что умненьких очень мало, а будет ещё меньше:).
Но, конечно, в проектах формальной верификации (крайне дорогих) только они и применяются (Coq, Lean, Agda...). Полагаю, что в итоге всё программирование к этому и сведётся: будет либо дерьмовый и дешёвый вайб-кодинг со школотой, либо дорогое качество (верификация AI-кода) с элитой. И никакого промежуточного слоя, и никакой возможности лифтинга на топовые уровни.
Думайте.
2. ad-hoc полиморфизм -- это зависимые типы.
3. Сабтайпинг ("наследование") -- это эквивалентность.
Circle -- подтип Shape. Везде, где ожидается Shape, можно использовать Circle.
Профит! )))
(На самом деле, тут немеряное количество засад даже на уровне базы SOLID, особенно по LSP; всё это подробно, с анализом в ФП, разбирал в большом гайде)
По-взрослому же, в HoTT используется эквивалентность типов и унивалентность. Если тип Circle можно преобразовать в тип Shape, то это преобразование считается "путём" между типами. А унивалентность гарантирует, что если такой путь существует, то он по сути и есть "правильное" "наследование". Другими словами, любое свойство, доказанное для всех Shape, автоматически выполняется и для Circle (потому что с точки зрения логики предикатов они находятся в отношении эквивалентности).
Классическое наследование -- это частный случай построения такого "пути-функции" из подтипа в супертип.
При этом мы получаем все "инженерные" фишки ООП (SOLID и Co) "в коробке", за нас всё делает HoTT-"движок". Например, в Shape есть area() (вычисление площади), которая всегда должна быть положительной. Но в реализации Circle она может быть нулевой, и тем самым мы нарушаем LSP.
В HoTT же "нарушить LSP" технически невозможно: система типов (топовая в мире на сегодня) гарантирует, что все случаи обработаны корректно. Подтипизация тут моделируется через эквивалентность, которая сохраняет все свойства: если какой-то подтип не удовлетворяет всем свойствам супертипа, то мы просто не сможем доказать эти свойства для супертипа, и значит, не сможем применить их к подтипу.
Другими словами, при нарушении LSP (и многих других солид-шмолид etc) мы получим ошибку компиляции.
=
Другое дело, что сегодня таких "языков программирования", реализующих HoTT (или хотя бы просто завтипы), которые можно было бы считать массовыми хотя бы на 2%, нету и особо не ожидается (в первую очередь потому, что умненьких очень мало, а будет ещё меньше:).
Но, конечно, в проектах формальной верификации (крайне дорогих) только они и применяются (Coq, Lean, Agda...). Полагаю, что в итоге всё программирование к этому и сведётся: будет либо дерьмовый и дешёвый вайб-кодинг со школотой, либо дорогое качество (верификация AI-кода) с элитой. И никакого промежуточного слоя, и никакой возможности лифтинга на топовые уровни.
Думайте.
1👍35❤17✍3🤔2
.
Облако драгоценностей за неделю.
Приватный клуб:
Пример важности хорошей статической системы типов, когда вы пишете много-много тестов, и тем более, когда применяете TDD...
Как легко и просто перейти от ООП к функциональному стилю, не меняя язык программирования...
Для донов-неначинающих:
Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим курсантам, но тут расширенные и дополненные версии.
57. Как правильно думать над моделью данных в проекте
Я большой сторонник информационной избыточности: лучше хранить больше информации, что делает модель ограничений более простой и более эффективной. Учёт ограничений — это тема, сильно отличающаяся от обычного программирования. И хотя на поддержание информационной избыточности требуются отдельные ресурсы (нужен код для её поддержки)...
Большинство из вас занимается хард-скиллами, но это тупиковый путь, когда речь начинает идти о зарплате 300к-500к-1 млн в месяц.
Вот что для этого надо, база 7 пунктов: ...
(все старые материалы для донов постепенно сгорают)
=
Первые сериалы из существенно переработанных и улучшенных материалов СильныхИдей (по сути три книги) доступны на бусти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
3. SOLID-25
4. Гайд Вайб-проектирование
🚀
=
Новые материалы для ментатов Лаборатории.
В СильныеИдеи добавлен материал "124) Снова о тестах и TDD"
Важные рекомендации по стилю и структуре правильных тестов.
💪🏻
Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.
"ЛаМПовое": квантовый мем, пишем игру на асме на bare metal, почему DL это топология, Миротворец2 - девчачий!
Облако драгоценностей за неделю.
Приватный клуб:
Пример важности хорошей статической системы типов, когда вы пишете много-много тестов, и тем более, когда применяете TDD...
Как легко и просто перейти от ООП к функциональному стилю, не меняя язык программирования...
Для донов-неначинающих:
Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим курсантам, но тут расширенные и дополненные версии.
57. Как правильно думать над моделью данных в проекте
Я большой сторонник информационной избыточности: лучше хранить больше информации, что делает модель ограничений более простой и более эффективной. Учёт ограничений — это тема, сильно отличающаяся от обычного программирования. И хотя на поддержание информационной избыточности требуются отдельные ресурсы (нужен код для её поддержки)...
Большинство из вас занимается хард-скиллами, но это тупиковый путь, когда речь начинает идти о зарплате 300к-500к-1 млн в месяц.
Вот что для этого надо, база 7 пунктов: ...
(все старые материалы для донов постепенно сгорают)
=
Первые сериалы из существенно переработанных и улучшенных материалов СильныхИдей (по сути три книги) доступны на бусти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
3. SOLID-25
4. Гайд Вайб-проектирование
🚀
=
Новые материалы для ментатов Лаборатории.
В СильныеИдеи добавлен материал "124) Снова о тестах и TDD"
Важные рекомендации по стилю и структуре правильных тестов.
💪🏻
Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.
"ЛаМПовое": квантовый мем, пишем игру на асме на bare metal, почему DL это топология, Миротворец2 - девчачий!
1❤34👍12😁3
Музыкальный бизнес никогда не вернётся к тому, чем он был, и уже совсем близко время, когда мы больше никогда не услышим действительно талантливых исполнителей. Власть и влияние перешло к технократам. И то, что мы сегодня называем "доходами от музыки", на самом деле на 98% идёт не авторам, а технологическим компаниям, которые совершенно не заинтересованы в процветании музыкальной сцены или здоровой культуры.
Самый прибыльный клиент для стриминговой платформы -- это человек, который платит за подписку, но не пользуется ею.
Следующий по доходности клиент -- пассивный слушатель, который позволяет платформе выбирать песни для него.
Другими словами, эти технологические компании сильно отличаются от традиционных музыкальных дистрибьюторов и розничных магазинчиков, которые стремились увеличивать количество восторженных и преданных поклонников.
Новый музыкальный технопорядок предпочитает пассивность и застой -- они заложены в их бизнес-модели.
"Этот мир – неизлечимая иллюзия. Это очень полезное и целительное прозрение, когда вам не нужно каждый день жить среди этих проклятых машин и неопровержимых реальностей, которые ведут себя в точности как настоящие."
-- Карл Юнг
Самый прибыльный клиент для стриминговой платформы -- это человек, который платит за подписку, но не пользуется ею.
Следующий по доходности клиент -- пассивный слушатель, который позволяет платформе выбирать песни для него.
Другими словами, эти технологические компании сильно отличаются от традиционных музыкальных дистрибьюторов и розничных магазинчиков, которые стремились увеличивать количество восторженных и преданных поклонников.
Новый музыкальный технопорядок предпочитает пассивность и застой -- они заложены в их бизнес-модели.
"Этот мир – неизлечимая иллюзия. Это очень полезное и целительное прозрение, когда вам не нужно каждый день жить среди этих проклятых машин и неопровержимых реальностей, которые ведут себя в точности как настоящие."
-- Карл Юнг
1💯40❤15👍7🫡5✍3
Предлагали за миллион рублей написать базовый прувер. Точнее, некий движок для формальной верификации. Или модел-чекер, хз, я в детали не вникал... На базе HoTT.
Ну как, за миллион.... Год работы фристайл за 100k/месяц, отчёты раз в месяц, и вообще никто не трогаетхоть целыми днями играй в HoMM и ACС .
Но я отказался: с (около)госами не хочу связываться принципиально, потом ещё и должен останешься, всю жизнь бесплатно сопровождать :)
Ну и цена раз в 5-10 должна быть больше.
А понадобилось, я так подозреваю, потому как если хочешь получить 4+ уровень доверия своей СЗИ, то нужно соответствовать приказу ФСТЭК России № 76 от 02.06.2020 по темке доказательства безопасности формальной математической модели твоей системы.
И кагбэ раньше практически официально рекомендовали Event-B and the Rodin Platform -- какую-то древнюю штуку 20-летней давности, созданную на гранты Евросоюза. Работает как плагин для Эклипса :) исходники до сих пор хостятся на сорсфорж...
Главное, Карл, "the use of set theory as a modelling notation"! Ну, да, тогда CIC и HoTT ещё не существовало, и что только не использовалось, кто во что горазд...
И вот под это дело (видимо, после 2022-го наступило какое-то прозрение :)
пацаны хочут "свой прувер" (дело-то благородное...).
Вообще, вряд ли в российской айтишке сегодня есть что-то более стратегически важное для КИИ -- и при этом абсолютно уязвимое -- чем "свой прувер". Сейчас всё, что есть в этой теме, активно развивается прежде всего европейскими организациями -- как в плане софта, так и в плане математики и, конечно, в плане обучения, со всеми вытекающими для РФ. Ну, да, пока опенсорс в основном...
В единственном русскоязычном чятике по соответствующим формальным технологиям все спецы работают за границей (от Европы и ОАЕ до США и Японии), или уже на чемоданах...
Как правильно: дать наконец МИАН и (последним) русским математикам денег на это всё. Пусть там сделают по-взрослому.
А впрочем, это же не миллиарды рублейраспиливать выбрасывать впустую на "свой игровой движок", "свой приставка" и прочие подобные темки, бессмысленные и бесполезные (если не вредные) для страны сами по себе. Это математика, тут думать надо, и особо не пропиаришься.
Ну как, за миллион.... Год работы фристайл за 100k/месяц, отчёты раз в месяц, и вообще никто не трогает
Но я отказался: с (около)госами не хочу связываться принципиально, потом ещё и должен останешься, всю жизнь бесплатно сопровождать :)
Ну и цена раз в 5-10 должна быть больше.
А понадобилось, я так подозреваю, потому как если хочешь получить 4+ уровень доверия своей СЗИ, то нужно соответствовать приказу ФСТЭК России № 76 от 02.06.2020 по темке доказательства безопасности формальной математической модели твоей системы.
И кагбэ раньше практически официально рекомендовали Event-B and the Rodin Platform -- какую-то древнюю штуку 20-летней давности, созданную на гранты Евросоюза. Работает как плагин для Эклипса :) исходники до сих пор хостятся на сорсфорж...
Главное, Карл, "the use of set theory as a modelling notation"! Ну, да, тогда CIC и HoTT ещё не существовало, и что только не использовалось, кто во что горазд...
И вот под это дело (видимо, после 2022-го наступило какое-то прозрение :)
пацаны хочут "свой прувер" (дело-то благородное...).
Вообще, вряд ли в российской айтишке сегодня есть что-то более стратегически важное для КИИ -- и при этом абсолютно уязвимое -- чем "свой прувер". Сейчас всё, что есть в этой теме, активно развивается прежде всего европейскими организациями -- как в плане софта, так и в плане математики и, конечно, в плане обучения, со всеми вытекающими для РФ. Ну, да, пока опенсорс в основном...
В единственном русскоязычном чятике по соответствующим формальным технологиям все спецы работают за границей (от Европы и ОАЕ до США и Японии), или уже на чемоданах...
Как правильно: дать наконец МИАН и (последним) русским математикам денег на это всё. Пусть там сделают по-взрослому.
А впрочем, это же не миллиарды рублей
2👍52❤11❤🔥4✍2
7 октября вышел наш любимый π-тончик 3.14
В мэйнстриме в основном восхищаются его скоростью, и она действительно хороша: CPython 3.14 топчик, многопоточный интерпретатор здорово допилили под нагрузку, а PyPy летает вообще безумно быстро. Питон по скорости реально начинает конкурировать с нодой, и даже в ряде случаев с растом!
Ну а мне больше всего понравилось вот это =>
Add a built-in implementation for HMAC (Keyed-Hashing for Message Authentication; RFC 2104) using formally verified code from the HACL* project. This implementation is used as a fallback when the OpenSSL implementation of HMAC is not available.
Тренд однако.
В мэйнстриме в основном восхищаются его скоростью, и она действительно хороша: CPython 3.14 топчик, многопоточный интерпретатор здорово допилили под нагрузку, а PyPy летает вообще безумно быстро. Питон по скорости реально начинает конкурировать с нодой, и даже в ряде случаев с растом!
Ну а мне больше всего понравилось вот это =>
Add a built-in implementation for HMAC (Keyed-Hashing for Message Authentication; RFC 2104) using formally verified code from the HACL* project. This implementation is used as a fallback when the OpenSSL implementation of HMAC is not available.
Тренд однако.
Python documentation
What’s new in Python 3.14
Editors, Adam Turner and Hugo van Kemenade,. This article explains the new features in Python 3.14, compared to 3.13. Python 3.14 was released on 7 October 2025. For full details, see the changelog...
🏆36🤔10⚡8❤🔥3🤝2
Заслушался сказок классный прошлогодний видосик "Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters"
где два пацанчика пиарят свой Mathematical Superintelligence :)
Harmonic: AI for Formal Mathematical Reasoning
С тех пор они подорожали раз в 10, почти до миллиарда долларов.
Ну, да, 90% в задачках MiniF2F, золотая медаль на IMO 2025 (5 из 6) и т.д.
Ну, да, оба со стэнфордским образованием, один даже у Тао учился, хотя потом сразу ушли в IT-AI-бизнес (беспилотные машинки и прочая попса...).
Ну, да, прикрутили теорем-прувер (завтипчики) Lean4.
Хотя так-то на выходе у них как не было ничего, так и нету что потрогать вживую. Только красивый пиар :)
Вакансия их понравилось: Part-time Lean Expert. Яб пошёл.
Фронт ищут под Expo (классная кстати кросс-платформная либа, не знал про такую)
А Research Engineer, Formal Methods вот на фуллтайм.
The initial focus of this position will be on advancing mathematical theorem proving using cutting-edge AI techniques. The successful candidate will play a key role in developing new algorithms and models that integrate AI with formal methods to solve complex problems in theorem proving and beyond.
Apply formal verification techniques using Lean or similar frameworks to formally verify safety critical systems
А решатели свои они пишут на плюсах: 17 из 30 сложных геометрических задач в AG-30 решены за 0.4 секунды на одном ядре 3.1 ГГц, и кодера тоже ищут (но и Python обязателен; у меня в Лаборатории теперь, кстати, тоже :).
Да, но...
For a while during the IMO, we had nearly 500,000 CPUs running Lean code at the same time with 95-100% utilization, which shows that the solution we built worked.
Вообще у них действительно немало больших и сложных научных(?) статей, где они типа достаточно подробно разбирают свои подходы, хотя подобные тексты сегодня не сложно генерить с хорошим AI, всё равно никто ничего не разберёт :)
Например свежак Aristotle: IMO-level Automated Theorem Proving
Мои 2 коп что их система смотрится уж слишком многоуровневой и перегруженной, с кучей слоёв абстракций. Сами судите:
- LLM-ка, обученная на Lean/SMT
- proof-search agent с деревом поиска и тактиками (имхо, самая слабая часть всей архитектуры - это архитектура самого Lean4, прежде всего концепция тактик)
- интеграция с лином через JSON-RPC
- версионированный датапайплайн self-play/self-mining
- RL с обратной связью от пруф-ассистента
- кэш фактов, бустинг через эвристики выбора лемм
- IDE-оболочка: чат, редактор с подсветкой, step-through доказательств, интеграция с Lean infoview
...
Главные вопросики:
- долгий и дорогой proof‑search + kernel‑check, возможно ли в принципе масштабировать на реальные кодобазы хотя бы в десятки тысяч строк кода?
- хрупкость по версии/ядру/тактикам Lean 4, да и сама его хилая экосистема и слабенькие датасеты вне mathlib
Ну и в целом насколько вообще переносятся "скиллы" решения математических задач на формальную верификацию? Получится ли хоть что-то перенести из хорошо формализованных задачек MiniF2F в суровый прод, тем более КИИ?
Так-то пайпу "Lean + генерация verification conditions + SMT/модел-чекинг" в принципе должно быть пофиг, что задачки, что верификация, но без очень мощного инженерного моста тут не обойтись, а в их проекте и так уже дофига всего накручено.
Наблюдение продолжаю 😎
где два пацанчика пиарят свой Mathematical Superintelligence :)
Harmonic: AI for Formal Mathematical Reasoning
С тех пор они подорожали раз в 10, почти до миллиарда долларов.
Ну, да, 90% в задачках MiniF2F, золотая медаль на IMO 2025 (5 из 6) и т.д.
Ну, да, оба со стэнфордским образованием, один даже у Тао учился, хотя потом сразу ушли в IT-AI-бизнес (беспилотные машинки и прочая попса...).
Ну, да, прикрутили теорем-прувер (завтипчики) Lean4.
Хотя так-то на выходе у них как не было ничего, так и нету что потрогать вживую. Только красивый пиар :)
Вакансия их понравилось: Part-time Lean Expert. Яб пошёл.
Фронт ищут под Expo (классная кстати кросс-платформная либа, не знал про такую)
А Research Engineer, Formal Methods вот на фуллтайм.
The initial focus of this position will be on advancing mathematical theorem proving using cutting-edge AI techniques. The successful candidate will play a key role in developing new algorithms and models that integrate AI with formal methods to solve complex problems in theorem proving and beyond.
Apply formal verification techniques using Lean or similar frameworks to formally verify safety critical systems
А решатели свои они пишут на плюсах: 17 из 30 сложных геометрических задач в AG-30 решены за 0.4 секунды на одном ядре 3.1 ГГц, и кодера тоже ищут (но и Python обязателен; у меня в Лаборатории теперь, кстати, тоже :).
Да, но...
For a while during the IMO, we had nearly 500,000 CPUs running Lean code at the same time with 95-100% utilization, which shows that the solution we built worked.
Вообще у них действительно немало больших и сложных научных(?) статей, где они типа достаточно подробно разбирают свои подходы, хотя подобные тексты сегодня не сложно генерить с хорошим AI, всё равно никто ничего не разберёт :)
Например свежак Aristotle: IMO-level Automated Theorem Proving
Мои 2 коп что их система смотрится уж слишком многоуровневой и перегруженной, с кучей слоёв абстракций. Сами судите:
- LLM-ка, обученная на Lean/SMT
- proof-search agent с деревом поиска и тактиками (имхо, самая слабая часть всей архитектуры - это архитектура самого Lean4, прежде всего концепция тактик)
- интеграция с лином через JSON-RPC
- версионированный датапайплайн self-play/self-mining
- RL с обратной связью от пруф-ассистента
- кэш фактов, бустинг через эвристики выбора лемм
- IDE-оболочка: чат, редактор с подсветкой, step-through доказательств, интеграция с Lean infoview
...
Главные вопросики:
- долгий и дорогой proof‑search + kernel‑check, возможно ли в принципе масштабировать на реальные кодобазы хотя бы в десятки тысяч строк кода?
- хрупкость по версии/ядру/тактикам Lean 4, да и сама его хилая экосистема и слабенькие датасеты вне mathlib
Ну и в целом насколько вообще переносятся "скиллы" решения математических задач на формальную верификацию? Получится ли хоть что-то перенести из хорошо формализованных задачек MiniF2F в суровый прод, тем более КИИ?
Так-то пайпу "Lean + генерация verification conditions + SMT/модел-чекинг" в принципе должно быть пофиг, что задачки, что верификация, но без очень мощного инженерного моста тут не обойтись, а в их проекте и так уже дофига всего накручено.
Наблюдение продолжаю 😎
❤36😎12✍3🐳3
Будь у меня миллиард миллион долларов рублей,
я бы прежде всего конечно перенёс мой HoTT/кубический движок на питончик 3.14, уже имея в отличие от стэнфордских пацанов
- тесную интеграцию со всем стеком PyTorch/JAX/NumPy -- для обучения тактик, ретривера лемм, RL с фидбэком от проверяющего ядра;
- полный контроль над trusted kernel/аксиоматикой HoTT (Univalence, HITs, кубические Сигмы, Kan-композиция) + быстрые эксперименты;
- гибкую архитектуру термов (de Bruijn/HOAS);
- программируемую генерацию синтетики: пути/ кубы/системы → мощные датасеты и property-based тестирование "из коробки".
Дальше,
- допиливаем кэширование/мемоизацию, тонкое профилирование (py-spy, tracers),
- легко и просто склеиваем с SMT/ATP (z3-solver, cvc5);
- добавляем нейросимволические циклы Generate→Check→Learn на одном Питоне!!1 Трассы поиска/ошибки элаборации/метаданные обучающих эпизодов -- у меня все под руками прямо в Py.
Фигак фигак и в прод: notebooks с визуализацией кубиков, REST/gRPC, и деплой через pip/docker без кривейшего тулчейна Lean.
я бы прежде всего конечно перенёс мой HoTT/кубический движок на питончик 3.14, уже имея в отличие от стэнфордских пацанов
- тесную интеграцию со всем стеком PyTorch/JAX/NumPy -- для обучения тактик, ретривера лемм, RL с фидбэком от проверяющего ядра;
- полный контроль над trusted kernel/аксиоматикой HoTT (Univalence, HITs, кубические Сигмы, Kan-композиция) + быстрые эксперименты;
- гибкую архитектуру термов (de Bruijn/HOAS);
- программируемую генерацию синтетики: пути/ кубы/системы → мощные датасеты и property-based тестирование "из коробки".
Дальше,
- допиливаем кэширование/мемоизацию, тонкое профилирование (py-spy, tracers),
- легко и просто склеиваем с SMT/ATP (z3-solver, cvc5);
- добавляем нейросимволические циклы Generate→Check→Learn на одном Питоне!!1 Трассы поиска/ошибки элаборации/метаданные обучающих эпизодов -- у меня все под руками прямо в Py.
Фигак фигак и в прод: notebooks с визуализацией кубиков, REST/gRPC, и деплой через pip/docker без кривейшего тулчейна Lean.
1❤36🔥17⚡5
Встретил сегодня этот мем и вспомнил в тему вчерашние посты.
Aristotle (an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems) так-то внутри использует Монте-Карло, Карл!
пруф: "Aristotle: IMO-level Automated Theorem Proving"
Ну, да, Monte Carlo Graph Search вместо традиционного MCTS, когда разные пути могут приходить в один и тот же proof state (т.к. Lean-цели часто повторяются и можно избежать комбинаторного взрыва из-за дублирования узлов + легче распараллеливать), но нету никакой математической гарантии найти глобально оптимальную (минимальную) последовательность тактик. Цель MCGS -- найти хоть какое-то корректное доказательство...
Вот тебе, бабушка, Mathematical Superintelligence и формальные рассуждения...
Aristotle (an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems) так-то внутри использует Монте-Карло, Карл!
пруф: "Aristotle: IMO-level Automated Theorem Proving"
Ну, да, Monte Carlo Graph Search вместо традиционного MCTS, когда разные пути могут приходить в один и тот же proof state (т.к. Lean-цели часто повторяются и можно избежать комбинаторного взрыва из-за дублирования узлов + легче распараллеливать), но нету никакой математической гарантии найти глобально оптимальную (минимальную) последовательность тактик. Цель MCGS -- найти хоть какое-то корректное доказательство...
Вот тебе, бабушка, Mathematical Superintelligence и формальные рассуждения...
❤43✍9😁1😇1
...Но с другой стороны, давайте будем максимально честными: нафига нам "свой прувер"? Чтобы получилось точно такая же ситуация, как и со "свой игровой движок" -- потратим миллиарды, а на выходе карго-культ?
Причём ещё ладно если так, а если это будет что-то существенно хуже работающее, чем существующий опенсорс, и к нему будут принуждать насильно? Тогда вместо формальной верификации наши КИИ получат ужасающее количество бэкдоров :)
И главное, а кто это будет делать-то? Последний наш мировой спец по HoTT уехал в Европу в 2023-м, а тут требуется не только топовая математика, но и мощнейший инженерный бэкграунд, чтобы не получился в итоге ещё более слабый клон Lean4 (который сам по себе кривейший и архитектурно и концептуально).
...Впрочем, а я-то чего об этом волнуюсь? Я в этих темах никто, и звать меня никак. С моей стороны это чисто научпоп. Поэтому, надо просто принять и простить, что Lean4 стал на сегодня в отрасли фактически промышленным стандартом. Да, очень кривейшим, примерно как Java на фоне нормальных языков, но лучше-то нету! Ну, Coq/Rocq, Agda, F*, но они уже очень сильно отстают просто потому, что в лине есть мощнейшая mathlib, куда уже впилили кучу математики, и продолжают активно накачивать.
Поэтому надеюсь, что свой прувер у нас делать не будут, потому что без матлибы он будет пшиком... Ну ок, можно делать синтаксически совместимым с лином, это значит и потащить за собой все его кривые фичи. Или писать свой конвертер, который ещё надо формально верифицировать, и т.д. и т.п.
Всё, поезд ушёл.
В связи с вышеизложенным с глубоким прискорбием вынужден сообщить, что я буду обучать (вас:) Lean4, коли даже стартапы чётко под него собирают по миллиарду долларов. И, конечно, это musthave, если вы математик и хотите укатить в европы америки...
Причём ещё ладно если так, а если это будет что-то существенно хуже работающее, чем существующий опенсорс, и к нему будут принуждать насильно? Тогда вместо формальной верификации наши КИИ получат ужасающее количество бэкдоров :)
И главное, а кто это будет делать-то? Последний наш мировой спец по HoTT уехал в Европу в 2023-м, а тут требуется не только топовая математика, но и мощнейший инженерный бэкграунд, чтобы не получился в итоге ещё более слабый клон Lean4 (который сам по себе кривейший и архитектурно и концептуально).
...Впрочем, а я-то чего об этом волнуюсь? Я в этих темах никто, и звать меня никак. С моей стороны это чисто научпоп. Поэтому, надо просто принять и простить, что Lean4 стал на сегодня в отрасли фактически промышленным стандартом. Да, очень кривейшим, примерно как Java на фоне нормальных языков, но лучше-то нету! Ну, Coq/Rocq, Agda, F*, но они уже очень сильно отстают просто потому, что в лине есть мощнейшая mathlib, куда уже впилили кучу математики, и продолжают активно накачивать.
Поэтому надеюсь, что свой прувер у нас делать не будут, потому что без матлибы он будет пшиком... Ну ок, можно делать синтаксически совместимым с лином, это значит и потащить за собой все его кривые фичи. Или писать свой конвертер, который ещё надо формально верифицировать, и т.д. и т.п.
Всё, поезд ушёл.
В связи с вышеизложенным с глубоким прискорбием вынужден сообщить, что я буду обучать (вас:) Lean4, коли даже стартапы чётко под него собирают по миллиарду долларов. И, конечно, это musthave, если вы математик и хотите укатить в европы америки...
🤔34✍12❤5🤯4
Ну и что тут непонятного, если вы проходили мой курс по ФП на F# ?
(а тем более, если трек по HoTT :)
Это малышовый пример по монадам со Стэнфордского курса
"CS 99: Functional Programming and Theorem Proving in Lean 4"
Вот что примерно будем делать(похищаю смыслы:) =>
The course project involves formalizing a non-trivial piece of mathematics or computer science in Lean 4.
(Easy) Formalize a solution to a (at least undergraduate level) textbook math or CS problem
(Medium) Formalize a board game that has not been done before. e.g. chess. The formalization should be at a level where it is possible to prove winning conditions.
(Medium) Formalize program verification primitives
(Medium) Formalize natural languages
(Hard) Contribute to Mathlib4 or other Lean formalization libraries
(Hard) Fix a Lean bug
Скоро будете у меня круче Гарварда-Стэнфорда :)
Техлиды, заглянув в ваш гитхаб, будут шептать "что ты такое??" :)
(а тем более, если трек по HoTT :)
Это малышовый пример по монадам со Стэнфордского курса
"CS 99: Functional Programming and Theorem Proving in Lean 4"
Вот что примерно будем делать
The course project involves formalizing a non-trivial piece of mathematics or computer science in Lean 4.
(Easy) Formalize a solution to a (at least undergraduate level) textbook math or CS problem
(Medium) Formalize a board game that has not been done before. e.g. chess. The formalization should be at a level where it is possible to prove winning conditions.
(Medium) Formalize program verification primitives
(Medium) Formalize natural languages
(Hard) Contribute to Mathlib4 or other Lean formalization libraries
(Hard) Fix a Lean bug
Скоро будете у меня круче Гарварда-Стэнфорда :)
Техлиды, заглянув в ваш гитхаб, будут шептать "что ты такое??" :)
😁41❤12⚡4🏆1
Что такое мэйнстрим? Это бессистемное множество абстракций, каждая из которых "упрощает" разработку для глупеньких, но увеличивает накладные расходы.
Типа,
React → API Gateway → Spring Boot → Docker → Kubernetes → VM → СУБД
Каждый слой добавляет "всего 20-30-50...%", и вот вы уже получили в 3-10 раз больше затрат на то же самое поведение.
Вот почему в системах, созданных мэйнстримом, утечка ресурсов (например, слив десятков гигов оперативки) это норм. Не потому, что кто-то специально наговнокодил (хотя и не без этого), а в основном потому, что никто не замечал совокупных затрат, пока пользователи не начали жаловаться.
Типа,
React → API Gateway → Spring Boot → Docker → Kubernetes → VM → СУБД
Каждый слой добавляет "всего 20-30-50...%", и вот вы уже получили в 3-10 раз больше затрат на то же самое поведение.
Вот почему в системах, созданных мэйнстримом, утечка ресурсов (например, слив десятков гигов оперативки) это норм. Не потому, что кто-то специально наговнокодил (хотя и не без этого), а в основном потому, что никто не замечал совокупных затрат, пока пользователи не начали жаловаться.
❤🔥30💯17👏8🤔6❤3
Вот чем в частности станем заниматься: будем формализовывать интуицию, которая по определению просто какая-то бессистемная мешанина случайно нахватанных знаний by examples. Глупенькая индукция: если некоторые части решения покрыты тестами (кусочками опыта, вайб-кодом...), "следовательно" оно верное в целом. Ага.
Делаем такое (с)мутное понимание эксплицитным, что даёт возможность за счёт непрерывного фидбэка его невероятно прокачивать вообще без пределов!!1
Как профессиональный пианист с консерваторским образованием может легко и просто играть любую музыку, так ты после гайдов с практикой на Lean4 сможешь уверенно выстраивать сложнейшие композиции паттернов/абстракций в любом языке, где есть минимальная поддержка функционального стиля (Python, C#, Java, PHP :).
Что имею в виду: джун в голове может удерживать одновременно 2-3 абстракции, может их скомпозировать на 1-2 уровня, а о том, что есть математические правила композиции, даже и не знает(ну, если только не занимался в моей Лаборатории :) . На отладку такой композиции тратит до 8 часов.
Миддл: 4-7 абстракций, 3-4 уровня композиции. Знает, что есть какие-то правила, но не всегда помнит, какие именно подойдут в той или иной ситуации. На создание/отладку - 4 часа.
Сеньор: 6-9 абстракций, 4-7 уровней композиции. Понимание законов: 30-50% (знает основные, интуитивно применяет). В основном методом проб и ошибок, рефакторинг может сломать его художества легко и просто. На создание/отладку - 1.5-2 часа.
Лаборатория: 10-15++ абстракций, 8-10++ уровней композиции. Понимание законов: 90-95% (можешь доказать, почему работает). И создаёшь такое буквально в режиме непрерывного набора текста, за полчаса.
На картинках: максимально простой детский учебный пример, уровень джуна ))) Reader, State и Except.
Спека на лине, и рабочий код на F#.
А самое главное, что вы получите суперсилу и станете AI-повелителем: сможете уверенно проектировать систему любой сложности через подобные композиции чистых функций, каждая из которых задаётся формальной (и полностью доказанной при желании) спецификацией, и соответственно LLM-ка пишет по ней гарантированно безошибочный код (вдобавок, это легко распраллеливается).
Свежие прогнозы, что к концу текущего десятилетия 90% кода будет писано AI, и думаю, это реально. Главный вопрос, какой процент архитектуры, software design будет приходиться на долю AI :) Полагаю, он будет резко падать по мере роста проекта. 3-5 тысяч строк кода standalone-система - ну возможно, AI потянет архитектуру. Десятки тысяч строк -- уже почти невероятно, сотни тысяч - фактически нет.
В этом плане крайне показательно, что AI (ЖПТ5Кодер) совсем слабенько пишет код на лине. После десятка подсказок еле-еле выдаёт что-то работающее более-менее сложное. А Клод4.5, что удивительно, вообще не тянет, ну совсем практически. Не способны они в принципе мыслить проектными абстракциями :)
Чем мне крайне нравится такой подход? Тем, что он впервые в мире в обучении сложным темкам в проектировании даёт гарантированный критерий правильности решения (за счёт сильной системы типов). Условно говоря, программа либо "компилируется" (доказывается, что она гарантированно правильная), и её можно использовать, либо нет (неработающая).
Я мечтал об этом давно, но вот только сейчас понял, как это сделать. Благодаря Филдсовскому лауреату Теренсу Тао, кстати, инсайт был после его подкаста "Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI" (есть автоматическая озвучка на русском).
Делаем такое (с)мутное понимание эксплицитным, что даёт возможность за счёт непрерывного фидбэка его невероятно прокачивать вообще без пределов!!1
Как профессиональный пианист с консерваторским образованием может легко и просто играть любую музыку, так ты после гайдов с практикой на Lean4 сможешь уверенно выстраивать сложнейшие композиции паттернов/абстракций в любом языке, где есть минимальная поддержка функционального стиля (Python, C#, Java, PHP :).
Что имею в виду: джун в голове может удерживать одновременно 2-3 абстракции, может их скомпозировать на 1-2 уровня, а о том, что есть математические правила композиции, даже и не знает
Миддл: 4-7 абстракций, 3-4 уровня композиции. Знает, что есть какие-то правила, но не всегда помнит, какие именно подойдут в той или иной ситуации. На создание/отладку - 4 часа.
Сеньор: 6-9 абстракций, 4-7 уровней композиции. Понимание законов: 30-50% (знает основные, интуитивно применяет). В основном методом проб и ошибок, рефакторинг может сломать его художества легко и просто. На создание/отладку - 1.5-2 часа.
Лаборатория: 10-15++ абстракций, 8-10++ уровней композиции. Понимание законов: 90-95% (можешь доказать, почему работает). И создаёшь такое буквально в режиме непрерывного набора текста, за полчаса.
На картинках: максимально простой детский учебный пример, уровень джуна ))) Reader, State и Except.
Спека на лине, и рабочий код на F#.
А самое главное, что вы получите суперсилу и станете AI-повелителем: сможете уверенно проектировать систему любой сложности через подобные композиции чистых функций, каждая из которых задаётся формальной (и полностью доказанной при желании) спецификацией, и соответственно LLM-ка пишет по ней гарантированно безошибочный код (вдобавок, это легко распраллеливается).
Свежие прогнозы, что к концу текущего десятилетия 90% кода будет писано AI, и думаю, это реально. Главный вопрос, какой процент архитектуры, software design будет приходиться на долю AI :) Полагаю, он будет резко падать по мере роста проекта. 3-5 тысяч строк кода standalone-система - ну возможно, AI потянет архитектуру. Десятки тысяч строк -- уже почти невероятно, сотни тысяч - фактически нет.
В этом плане крайне показательно, что AI (ЖПТ5Кодер) совсем слабенько пишет код на лине. После десятка подсказок еле-еле выдаёт что-то работающее более-менее сложное. А Клод4.5, что удивительно, вообще не тянет, ну совсем практически. Не способны они в принципе мыслить проектными абстракциями :)
Чем мне крайне нравится такой подход? Тем, что он впервые в мире в обучении сложным темкам в проектировании даёт гарантированный критерий правильности решения (за счёт сильной системы типов). Условно говоря, программа либо "компилируется" (доказывается, что она гарантированно правильная), и её можно использовать, либо нет (неработающая).
Я мечтал об этом давно, но вот только сейчас понял, как это сделать. Благодаря Филдсовскому лауреату Теренсу Тао, кстати, инсайт был после его подкаста "Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI" (есть автоматическая озвучка на русском).
2❤35✍13👍6❤🔥1
Сами задачки на композицию в Lean4 -- это по сути логические паззлы в чистом виде! Но чётко заточенные под скилл software design, вдобавок при их решении целевым образом качаем профильную когнитивку! Я много изучал десятки тренажёров "развитие внимательности, памяти, ...", коих в сети немеряно, но таких что хоть немного подходили бы программистской работе, и близко не встречал. А тут такая удача.
...Но есть две мааалюсенькие проблемки :)
1. В создании соответствующих задачек, конкретно под темку software design, никакой AI, к сожалению не поможет. Практика показала, что он в основном больше вредит :) Проблема чисто техническая, просто потребуется вложить существенно больше времени (увы).
2. Платформа (Lean4) тоже имеет определённое значение. В частности большой вопрос, какие теории типов поддерживает прувер. Lean4 например не способен в HoTT из-за своего кривого ядра вывода. Ну и экосистема имеет значение: похоже, Лин взял всё самое худшее из экосистемы Хаскеля :) Попробуйте например собрать Mathlib в винде.
Поэтому сами задачки мне придётся сперва делать в некоторой мета-теории, без привязки к конкретным теорем-пруверам или языкам с зависимыми типами, чтобы их (как "реализацию" без изменения интерфейсов) можно было безболезненно заменять в случае чего. Можно теоркат (симплициальные ∞-категории), можно кубическую теорию типов, благо я сделал её "реализацию"...
Насколько это всё сложно в плане понимания? Ну, смотрю разные математические семинары, это например третий курс мехмата НГУ.
...Но есть две мааалюсенькие проблемки :)
1. В создании соответствующих задачек, конкретно под темку software design, никакой AI, к сожалению не поможет. Практика показала, что он в основном больше вредит :) Проблема чисто техническая, просто потребуется вложить существенно больше времени (увы).
2. Платформа (Lean4) тоже имеет определённое значение. В частности большой вопрос, какие теории типов поддерживает прувер. Lean4 например не способен в HoTT из-за своего кривого ядра вывода. Ну и экосистема имеет значение: похоже, Лин взял всё самое худшее из экосистемы Хаскеля :) Попробуйте например собрать Mathlib в винде.
Поэтому сами задачки мне придётся сперва делать в некоторой мета-теории, без привязки к конкретным теорем-пруверам или языкам с зависимыми типами, чтобы их (как "реализацию" без изменения интерфейсов) можно было безболезненно заменять в случае чего. Можно теоркат (симплициальные ∞-категории), можно кубическую теорию типов, благо я сделал её "реализацию"...
Насколько это всё сложно в плане понимания? Ну, смотрю разные математические семинары, это например третий курс мехмата НГУ.
❤36👍12⚡6✍1
.
Облако драгоценностей за неделю.
Для донов-начинающих:
На 98%, конечно, программирование — это просто ...
В мире конкуренции препятствия — ваш союзник. Чем труднее они, тем выше ваши шансы избавиться от конкурентов :) Если же эти препятствия заставляют и вас отступить, что ж, выходит, всё было зря...
Для донов-неначинающих:
Меня всегда поражало, сколь многого человек может достичь, если просто...
Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим курсантам, но тут расширенные и дополненные версии.
58. О вреде форматов сериализации
Структуры данных, определяемые на языках вроде IDL и его расширения OpenAPI, или в конфигурационных файлах -- это формат сериализации. Но формат сериализации не имеет никакого отношения к модели данных проекта!..
59. Что делает тест хорошим
Есть прекрасная теория тестирования, которая объясняет, что делают тесты, что должно и что не должно проверяться при тестировании. Увы, это удивительно, но эта теория практически не была представлена в общедоступном виде для массовых разработчиков, хотя я подозреваю, что определённое количество инженеров, применяющих подходы из формальной верификации, имеют достаточно чёткое представление об этом...
(все старые материалы для донов постепенно сгорают)
=
Первые сериалы из существенно переработанных и улучшенных материалов СильныхИдей (по сути три книги) доступны на бусти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
3. SOLID-25
4. Гайд Вайб-проектирование
🚀
=
Новые материалы для ментатов Лаборатории.
В курс карьеры добавлен 115-й материал "Выбираем правильный путь для карьеры и жизни".
Вот главный урок, который я подсознательно усваивал на протяжении нескольких десятков лет своей карьеры, преодолевая бесчисленные оплошности и моменты сомнений (и только в последние годы я по-настоящему начал прислушиваться к своим собственным знаниям и советам, чему невероятно рад :)...
Python на сервере обновлён до 3.14 (и всем рекомендую перейти на эту версию).
В раздел "Элитный программист" добавлен материал
78) Почему Pomodoro -- лучшая техника для работы!
Почему техника помидорок структурирована именно так? Почему она состоит из 25-минутных фрагментов работы? На чём она основана на самом деле?
Продолжительность продуктивных циклов в Помодоро определяется двумя факторами...
💪🏻
Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.
=
Облако драгоценностей за неделю.
Для донов-начинающих:
На 98%, конечно, программирование — это просто ...
В мире конкуренции препятствия — ваш союзник. Чем труднее они, тем выше ваши шансы избавиться от конкурентов :) Если же эти препятствия заставляют и вас отступить, что ж, выходит, всё было зря...
Для донов-неначинающих:
Меня всегда поражало, сколь многого человек может достичь, если просто...
Продолжаю выкладывать для донов материалы СильныхИдей — доступны моим курсантам, но тут расширенные и дополненные версии.
58. О вреде форматов сериализации
Структуры данных, определяемые на языках вроде IDL и его расширения OpenAPI, или в конфигурационных файлах -- это формат сериализации. Но формат сериализации не имеет никакого отношения к модели данных проекта!..
59. Что делает тест хорошим
Есть прекрасная теория тестирования, которая объясняет, что делают тесты, что должно и что не должно проверяться при тестировании. Увы, это удивительно, но эта теория практически не была представлена в общедоступном виде для массовых разработчиков, хотя я подозреваю, что определённое количество инженеров, применяющих подходы из формальной верификации, имеют достаточно чёткое представление об этом...
(все старые материалы для донов постепенно сгорают)
=
Первые сериалы из существенно переработанных и улучшенных материалов СильныхИдей (по сути три книги) доступны на бусти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
3. SOLID-25
4. Гайд Вайб-проектирование
🚀
=
Новые материалы для ментатов Лаборатории.
В курс карьеры добавлен 115-й материал "Выбираем правильный путь для карьеры и жизни".
Вот главный урок, который я подсознательно усваивал на протяжении нескольких десятков лет своей карьеры, преодолевая бесчисленные оплошности и моменты сомнений (и только в последние годы я по-настоящему начал прислушиваться к своим собственным знаниям и советам, чему невероятно рад :)...
Python на сервере обновлён до 3.14 (и всем рекомендую перейти на эту версию).
В раздел "Элитный программист" добавлен материал
78) Почему Pomodoro -- лучшая техника для работы!
Почему техника помидорок структурирована именно так? Почему она состоит из 25-минутных фрагментов работы? На чём она основана на самом деле?
Продолжительность продуктивных циклов в Помодоро определяется двумя факторами...
💪🏻
Мы здесь, потому что это трудно.
it's a privilege to do things that are hard.
=
❤33👍11