ВШЭ подняла цену на обучение, внимание, прикладной математике! (этому реально трудно учиться, по себе знаю 💪🏻) с 467 до 767 тысяч рублей за год учёбы.
Но главное конечно, что спрос на эти темки ощутимо растёт, и это прекрасно ❤️
Даже, думаю, стратегически, на 51% сместить акцент на математику, конкретно в контексте программирования конечно, но всё же по достаточно серьёзным темам 🤓
Вчерашний отзыв от ментата, приближающегося к уровню Гипотетик (подготовительное перед гайдом по гомотопической теории 🚀):
Я прочитал книгу "Типы в языках программирования" (Пирс).
Особенно интересными для меня были следующие моменты:
1) Константы Чёрча в лямбда-исчислении.
Всегда воспринимал константы как "атомы", а оказалось, что их можно составить из более низкоуровневых конструкций.
2) Соотношение Карри-Говарда между логикой и типами.
Вот, оказывается, как теория типов связана с доказательством теорем.
3) Помимо типов в какой-то момент появляются виды, которые относятся к типам примерно как типы - к значениям.
При этом типы с видами не смешиваются.
Совсем недавно из других книг по математике я узнал, что явное разделение таких вещей используется, чтобы избежать парадоксов в теории множеств.
Математика для меня не будет прежней :)
p.s. Хотите, индивидуально буду обучать по курсам вшэ, мехмата, физтеха, спбгу? mit, cmu, оксфорд гарвард :)
❤️❤️❤️
Но главное конечно, что спрос на эти темки ощутимо растёт, и это прекрасно ❤️
Даже, думаю, стратегически, на 51% сместить акцент на математику, конкретно в контексте программирования конечно, но всё же по достаточно серьёзным темам 🤓
Вчерашний отзыв от ментата, приближающегося к уровню Гипотетик (подготовительное перед гайдом по гомотопической теории 🚀):
Я прочитал книгу "Типы в языках программирования" (Пирс).
Особенно интересными для меня были следующие моменты:
1) Константы Чёрча в лямбда-исчислении.
Всегда воспринимал константы как "атомы", а оказалось, что их можно составить из более низкоуровневых конструкций.
2) Соотношение Карри-Говарда между логикой и типами.
Вот, оказывается, как теория типов связана с доказательством теорем.
3) Помимо типов в какой-то момент появляются виды, которые относятся к типам примерно как типы - к значениям.
При этом типы с видами не смешиваются.
Совсем недавно из других книг по математике я узнал, что явное разделение таких вещей используется, чтобы избежать парадоксов в теории множеств.
Математика для меня не будет прежней :)
p.s. Хотите, индивидуально буду обучать по курсам вшэ, мехмата, физтеха, спбгу? mit, cmu, оксфорд гарвард :)
❤️❤️❤️
3❤57🔥12👍7🫡7😁1
Риторическое.
1. Почему национальный менеджер называется по-английски MAX (сразу в нарушении нескольких законов) ?
2. Но даже если как его иногда пишут МАКС, нарушается правило русского языка в отношении имён собственных (которое изучается во втором классе началки): имеет право только начинаться с заглавной буквы (например, Макс), а лепет про "ну ммм ээээ а это у нас вот такое название крупненьким пишем, вот у нас так принято" отдел маркетинга может засунуть себе ... ?
1. Почему национальный менеджер называется по-английски MAX (сразу в нарушении нескольких законов) ?
2. Но даже если как его иногда пишут МАКС, нарушается правило русского языка в отношении имён собственных (которое изучается во втором классе началки): имеет право только начинаться с заглавной буквы (например, Макс), а лепет про "ну ммм ээээ а это у нас вот такое название крупненьким пишем, вот у нас так принято" отдел маркетинга может засунуть себе ... ?
😁47👍12🤔8🤓4✍2
Просили пояснить за валютные блоги: там оказывается какая-то кривейшая платёжная система "страйп": если вы не эээ резидент и не имеете ein, то фиг там зарегитесь. Действительно даже если у вас счёт в крупном западном банке (не американском), то всё равно совсем не факт, что сабстэк вас застрайпонит: потребуется скорее всего предоставить инфу о юридическом статусе и т.п.
При том что есть шикарные аналоги -- например Ghost, который превосходит Substack по возможностям на порядок.
И тем не менее это очень наглядный пример того, что сабстэк в текстовых блогах сегодня как ютуб в видео: какие усилия не прикладывай, теперь уже в принципе не догнать даже на 2%.
Это уже огромное количество контента, тесно связанное с системой рекомендаций, кросс-постингом и множеством других инструментов, которые упрощают органический рост.
(а у нас ВК обрезает охваты теперь вообще до нуля... вообще, законодательно надо их обязать, коли монополисты, гарантированный показ каждого поста всем подписчикам в течение 48 часов.)
... А впрочем, платформа, напомню, это просто технический инструмент. До уровня 1.000.000 руб в месяц на платном блоге вы можете взять вообще что угодно - вк, тг, бусти, гхост...
Надо работать на более высоком уровне абстракции, и в первую очередь определить свою ПЛАТЯЩУЮ ЦА.
Звезда современного бурлеска Дита фон Тиз однажды рассказала, чему она научилась в самом начале своей карьеры стриптизерши в Лос Анджелесе. Ее коллеги – пергидрольные блондинки танцовщицы с искусственным загаром, бразильской эпиляцией и в бикини неоновых цветов – раздевались догола, если в клубе было пятьдесят мужчин, и каждый из них давал им по доллару. Дита появлялась на сцене в атласных перчатках, корсете и пачке, исполняла зажигательный танец и раздевалась до нижнего белья, чем приводила зрителей в недоумение. Но после этого, несмотря на то, что сорок девять мужчин ее игнорировали, находился один, который давал ей пятьдесят долларов.
Этот мужчина, по словам Диты, и был ее аудиторией.
Тим Феррис, "На плечах гигантов"
При том что есть шикарные аналоги -- например Ghost, который превосходит Substack по возможностям на порядок.
И тем не менее это очень наглядный пример того, что сабстэк в текстовых блогах сегодня как ютуб в видео: какие усилия не прикладывай, теперь уже в принципе не догнать даже на 2%.
Это уже огромное количество контента, тесно связанное с системой рекомендаций, кросс-постингом и множеством других инструментов, которые упрощают органический рост.
(а у нас ВК обрезает охваты теперь вообще до нуля... вообще, законодательно надо их обязать, коли монополисты, гарантированный показ каждого поста всем подписчикам в течение 48 часов.)
... А впрочем, платформа, напомню, это просто технический инструмент. До уровня 1.000.000 руб в месяц на платном блоге вы можете взять вообще что угодно - вк, тг, бусти, гхост...
Надо работать на более высоком уровне абстракции, и в первую очередь определить свою ПЛАТЯЩУЮ ЦА.
Звезда современного бурлеска Дита фон Тиз однажды рассказала, чему она научилась в самом начале своей карьеры стриптизерши в Лос Анджелесе. Ее коллеги – пергидрольные блондинки танцовщицы с искусственным загаром, бразильской эпиляцией и в бикини неоновых цветов – раздевались догола, если в клубе было пятьдесят мужчин, и каждый из них давал им по доллару. Дита появлялась на сцене в атласных перчатках, корсете и пачке, исполняла зажигательный танец и раздевалась до нижнего белья, чем приводила зрителей в недоумение. Но после этого, несмотря на то, что сорок девять мужчин ее игнорировали, находился один, который давал ей пятьдесят долларов.
Этот мужчина, по словам Диты, и был ее аудиторией.
Тим Феррис, "На плечах гигантов"
🔥37✍14😁6👌3🤔2
Есть такой умник, французский математик Thierry Coquand, один из главных авторов легендарного теорем-прувера Coq (Thierry и назвал его так по своей фамилии), который теперь Rocq -- ключевой инструмент в европейских университетах по обучению всяческим формальным темкам, и куда нам теперь путь навсегда заказан.
В основу своего петушка Кокан заложил собственную теорию типов Calculus of Constructions (CoC): типизированное λ-исчисление + логика высшего порядка + полиморфизм, через изоморфизм Карри-Ховарда.
И это конечно топчик λ-куба Барендрегта, да, но...
В CoC эквивалентность типов (изоморфизм) не означает их равенство. А вот гомотопическая теория типов Воеводского HoTT вводит аксиому унивалентности, которая отождествляет эквивалентные типы.
В CoC равенство определяется через лейбницевский принцип неразличимости тождественного. В HoTT он заменяется на тип путей Path (непрерывная деформация), а доказательства равенства становятся конструктивными (например, гомотопии), что позволяет естественно кодировать высшие категории или ∞-группоиды например. При этом сохраняется canonicity: программы на основе HoTT можно выполнять, а доказательства верифицируются алгоритмически.
хотт - это язык программирования Бога
Владимир Воеводский реализовал свои гениальные идеи HoTT в библиотеке Coq через расширение CIC (Calculus of Inductive Constructions). Он по сути трансформировал применение Coq, показав, что формальные системы могут кодировать не только логику, но и глубокие геометрические структуры.
Но в итоге два ведущих теорем-прувера + языка с заптипчиками - Coq/Rocq и Lean - решили развиваться в направлении усиления CIC, и по сути отказались от HoTT в своих движках, во многом из-за их архитектурной кривизны. По большому счёту это стратегическая ошибка, пояснял тут.
И это прям очень-очень радует 💥💥💥
В основу своего петушка Кокан заложил собственную теорию типов Calculus of Constructions (CoC): типизированное λ-исчисление + логика высшего порядка + полиморфизм, через изоморфизм Карри-Ховарда.
И это конечно топчик λ-куба Барендрегта, да, но...
В CoC эквивалентность типов (изоморфизм) не означает их равенство. А вот гомотопическая теория типов Воеводского HoTT вводит аксиому унивалентности, которая отождествляет эквивалентные типы.
В CoC равенство определяется через лейбницевский принцип неразличимости тождественного. В HoTT он заменяется на тип путей Path (непрерывная деформация), а доказательства равенства становятся конструктивными (например, гомотопии), что позволяет естественно кодировать высшие категории или ∞-группоиды например. При этом сохраняется canonicity: программы на основе HoTT можно выполнять, а доказательства верифицируются алгоритмически.
хотт - это язык программирования Бога
Владимир Воеводский реализовал свои гениальные идеи HoTT в библиотеке Coq через расширение CIC (Calculus of Inductive Constructions). Он по сути трансформировал применение Coq, показав, что формальные системы могут кодировать не только логику, но и глубокие геометрические структуры.
Но в итоге два ведущих теорем-прувера + языка с заптипчиками - Coq/Rocq и Lean - решили развиваться в направлении усиления CIC, и по сути отказались от HoTT в своих движках, во многом из-за их архитектурной кривизны. По большому счёту это стратегическая ошибка, пояснял тут.
И это прям очень-очень радует 💥💥💥
2😁29🤯16👍13❤9🤔6
.
Развиваю импортозамес и техноcуверен: пишу русский теорем-прувер с Z-типами.
Российских миллиардеров в Forbes полно, а я такой один.
Десятки миллионов евро, которые INRIA и евроуниверы вкладывают в Rocq на базе Calculus of Inductive Constructions (а Пентагон -- в Lean) -- это уже детский сад аспирантские штаны на лямках.
Переиграть и уничтожить.
За 2 часа и 15 долларов с Клодом4 я запилил всю эту хвалёную французскую петушатину CoC за 70 (семьдесят) строк кода на F# (+ вся мощща .NET прилагается).
Идеально для обучения, сделаю следующим гайдом по HoTT, перед "кубиками". В принципе, всего Барендрегта надо будет со временем запилить.
Развиваю импортозамес и техноcуверен: пишу русский теорем-прувер с Z-типами.
Российских миллиардеров в Forbes полно, а я такой один.
Десятки миллионов евро, которые INRIA и евроуниверы вкладывают в Rocq на базе Calculus of Inductive Constructions (а Пентагон -- в Lean) -- это уже детский сад аспирантские штаны на лямках.
Переиграть и уничтожить.
За 2 часа и 15 долларов с Клодом4 я запилил всю эту хвалёную французскую петушатину CoC за 70 (семьдесят) строк кода на F# (+ вся мощща .NET прилагается).
Идеально для обучения, сделаю следующим гайдом по HoTT, перед "кубиками". В принципе, всего Барендрегта надо будет со временем запилить.
4🏆50🤔17👍12🤯9😁5
-- Сергей Игоревич, меня иногда спрашивают "а зачем ты это всё учишь?" (например, математику), и я не знаю что ответить.
Честно, я сам даже не знаю, что ответить на вопрос "что ответить?", для меня это просто Кэп Очевидность.
Я например всю жизнь учусь для того чтобы становиться умнее, и это мне очень здорово всю жизнь помогает. И для меня вообще очень странно, что может быть по-другому.
Ну, да, у тех, кто задаёт вопросы "а зачем учиться [чему угодно]?", с развитием умишка как раз по определению большие проблемы. Глупенькие просто по жизни.
Можете ответить так например: "количество извилин в мозгу у определённых групп людей различается столь сильно, что это по сути формально разные виды животных". Ну как минимум, разные касты.
Честно, я сам даже не знаю, что ответить на вопрос "что ответить?", для меня это просто Кэп Очевидность.
Я например всю жизнь учусь для того чтобы становиться умнее, и это мне очень здорово всю жизнь помогает. И для меня вообще очень странно, что может быть по-другому.
Ну, да, у тех, кто задаёт вопросы "а зачем учиться [чему угодно]?", с развитием умишка как раз по определению большие проблемы. Глупенькие просто по жизни.
Можете ответить так например: "количество извилин в мозгу у определённых групп людей различается столь сильно, что это по сути формально разные виды животных". Ну как минимум, разные касты.
3😁43👍21💯10🤔5🐳2
Лайфхак если вас возвращают в офис с удалёнки, или вообще работа представляет собой концлагерь опенспейса.
Нет ничего лучше, чем постоянные громкие и нервные выкрики из своего уголка. Как автономные "WTF???", регулярно отвлекающие соседних коллег (матюшки тоже хорошо заходят, можно также позаикаться для особого нервирования окружающих), так и вопли на другой конец:
-- Олег, ... твою мать! Какого хера ты возвращаешь 500 на мой огромный джсон?
На каждую просьбу менеджеров "потише пожалуйста!" отвечайте одной и той же фразой "Хочите тишины? Возвращайте удалёнку, а я по другому не умею работать".
На "общайтесь в чате" -- "а нафига тогда нас призвали в офис??".
Недовольство соседних разработчиков просто откровенно игнорируйте. При этом регулярно качайтесь, снимая для верности пиджак, стригитесь налысо и обклеивайте стенки своего места лейблами бокса и ММА.
Можно также приходить в вызывающей одежде (шорты и шлёпки прям топчик будет).
Нет ничего лучше, чем постоянные громкие и нервные выкрики из своего уголка. Как автономные "WTF???", регулярно отвлекающие соседних коллег (матюшки тоже хорошо заходят, можно также позаикаться для особого нервирования окружающих), так и вопли на другой конец:
-- Олег, ... твою мать! Какого хера ты возвращаешь 500 на мой огромный джсон?
На каждую просьбу менеджеров "потише пожалуйста!" отвечайте одной и той же фразой "Хочите тишины? Возвращайте удалёнку, а я по другому не умею работать".
На "общайтесь в чате" -- "а нафига тогда нас призвали в офис??".
Недовольство соседних разработчиков просто откровенно игнорируйте. При этом регулярно качайтесь, снимая для верности пиджак, стригитесь налысо и обклеивайте стенки своего места лейблами бокса и ММА.
Можно также приходить в вызывающей одежде (шорты и шлёпки прям топчик будет).
1😁72❤10🔥8🤔2🐳1
.
Утром немного соберёшься в себя; но потом дело за делом развлекают тебя и к вечеру являешься пуст, омрачён и уныл; как быть? погиб я...
Старайся, по силе своей, не опутывать себя мелочными делами, ограничиваясь самонужнейшим.
прп. Варсонофий Великий
Нужнейшее на выхи: поиграть в правильные игры. Прочитал что (якобы) в Казахстане хотят запретить все игры кроме развивающих образовательных и пазлов, дико поддерживаю 💯
Ну может быть не столь категорично к этим жанрам добавить ещё небольшой "белый список": дота2, dune 2, starcraft ][, assetto corsa и dune awakening(ну ладно, и контру:) .
А так, 99,999% всего этого геймерского кала. включая приставки всех видов 💩 в топку, и вместе с ними забанить и все эти онлайн-кинотеатры с бесконечным киносериальным мусором 🤮 (да ещё и укравшие у народа ЛЧ ⚽️).
=
Вот белый список (lvl 1) разрешённых игр Лаборатории, которые каждому ментату абсолютно обязательно пройти до конца.
1) Развитие топологического мышления.
- Monument Valley все серии (22 июля выходит v3, срочно ставим в вишлисты);
- The Bridge (я иногда думал, ну вообще невозможно)
2) Развитие мета-мышления.
- Baba Is You
Утром немного соберёшься в себя; но потом дело за делом развлекают тебя и к вечеру являешься пуст, омрачён и уныл; как быть? погиб я...
Старайся, по силе своей, не опутывать себя мелочными делами, ограничиваясь самонужнейшим.
прп. Варсонофий Великий
Нужнейшее на выхи: поиграть в правильные игры. Прочитал что (якобы) в Казахстане хотят запретить все игры кроме развивающих образовательных и пазлов, дико поддерживаю 💯
Ну может быть не столь категорично к этим жанрам добавить ещё небольшой "белый список": дота2, dune 2, starcraft ][, assetto corsa и dune awakening
А так, 99,999% всего этого геймерского кала. включая приставки всех видов 💩 в топку, и вместе с ними забанить и все эти онлайн-кинотеатры с бесконечным киносериальным мусором 🤮 (да ещё и укравшие у народа ЛЧ ⚽️).
=
Вот белый список (lvl 1) разрешённых игр Лаборатории, которые каждому ментату абсолютно обязательно пройти до конца.
1) Развитие топологического мышления.
- Monument Valley все серии (22 июля выходит v3, срочно ставим в вишлисты);
- The Bridge (я иногда думал, ну вообще невозможно)
2) Развитие мета-мышления.
- Baba Is You
2😁43❤18✍8🥰2🐳2
математика тебе в программировании никогда не понадобится , говорили они... и даже знать представление чисел хотя бы на уровне сишечки тоже нафиг не нужно...
вот один из сотен анти-примеров: в idle-играх гигантские чиселки это норма например, но BigInteger поддерживает только целочисленное деление.
x / y — как это сделаешь?
Я исходно взял decimal (10^28 с точностью 100%), хотя сразу сильно сомневался, и не зря: для ачивки "Архитектор Цифровой Реальности" например потребуется 50.000 октиллионов (и это далеко не предел; после нескольких взломов Матрицы счёт крипты пойдёт на вигинтиллионы).
Как обычно надо было следовать собственным рекомендациям с "Быстрой прокачки ООП": любой сомнительный базовый/стандартный тип надо сразу же оборачивать своим типом во избежание. А в результате 2 часа рефакторил, и снова надо тестить нюансы.
По-взрослому конечно, вообще надо было полностью свою алгебру биг чисел смоделировать, через гомоморфизм мультипликативных групп.
Ведь логарифм — это просто изоморфизм между мультипликативной группой положительных чисел и аддитивной группой вещественных чисел...
вот один из сотен анти-примеров: в idle-играх гигантские чиселки это норма например, но BigInteger поддерживает только целочисленное деление.
BigInteger x, y;
x / y — как это сделаешь?
double result = (double)x / y; // <= детский сад; в дабле мантисса 53 бита
double result = Math.Exp(BigInteger.Log(x) - BigInteger.Log(y));
Я исходно взял decimal (10^28 с точностью 100%), хотя сразу сильно сомневался, и не зря: для ачивки "Архитектор Цифровой Реальности" например потребуется 50.000 октиллионов (и это далеко не предел; после нескольких взломов Матрицы счёт крипты пойдёт на вигинтиллионы).
Как обычно надо было следовать собственным рекомендациям с "Быстрой прокачки ООП": любой сомнительный базовый/стандартный тип надо сразу же оборачивать своим типом во избежание. А в результате 2 часа рефакторил, и снова надо тестить нюансы.
По-взрослому конечно, вообще надо было полностью свою алгебру биг чисел смоделировать, через гомоморфизм мультипликативных групп.
Ведь логарифм — это просто изоморфизм между мультипликативной группой положительных чисел и аддитивной группой вещественных чисел...
1❤30🤯25🤔11🔥4😁4
...Так вот чем в итоге ожидаемо закончился весь этот хайп "AI скоро заменит программистов": жпт просто стал must have скиллом, наряду с каким-нибудь кубером, который ранее был отдельной профессией; от программистов на работе стали требовать уметь и делать в x10...x100 раз больше, а зарплаты при этом даже немножечко понижаются.
А с другой стороны...
Пол почувствовал, что опять угодил в слепое время...
Этого момента он ещё не видел... только... только... где-то впереди раскачивалось чёрно-зелёное знамя Математики. Маячили обагрённые джихадом теорем-пруверы, бушевали легионы фанатиков гомотопической теории...
-- Этому не бывать, - прошептал он. -- Я не допущу.
А с другой стороны...
Пол почувствовал, что опять угодил в слепое время...
Этого момента он ещё не видел... только... только... где-то впереди раскачивалось чёрно-зелёное знамя Математики. Маячили обагрённые джихадом теорем-пруверы, бушевали легионы фанатиков гомотопической теории...
-- Этому не бывать, - прошептал он. -- Я не допущу.
2😁39⚡12🤔6❤3🏆1
.
Облако драгоценностей за неделю.
Набор ментатов в Лабораторию на 2025-й год закончен.
(регулярно думаю о том, как становиться меньше и постепенно исчезать из Сети)
Основной паблик:
Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).
Засада с микросервисами
Предыдущие серии:
Засада с исключениями
Засада с инициализацией
Засада с контроллером
Для донов-начинающих:
...Вопрос уже не о том, заменит ли нас искусственный интеллект, а в том, кто быстрее всего освоит искусственный интеллект своих целях. И одна из недооценённых областей интересов, о которой, как мне кажется, говорят недостаточно — это ОБРАЗОВАНИЕ.
6 рекомендаций + промпты для начинающих и всех желающих продуктивно самообучаться.
...Такой простой подход за короткое время -- месяцы, а может даже и недели -- далеко продвинет вас в IT в эпоху AI. Большинство разработчиков до сих пор понятия не имеют об огромных преимуществах использования искусственного интеллекта.
Для донов-неначинающих:
СильныеИдеи++
42. SOLID25 : [2...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.
Продолжение трека "Элитный программист":
29) Как соцсети помогут вам в создании личного бренда.
Вы можете быть элитным программистом с отличными навыками общения и работы в команде, но если ваши публичные профили в соцсетях выглядят плохо, никто не захочет брать вас на работу...
Золотые правила карьеры разработчика.
1. [...]. Идеальный вариант, когда тратишь на рабочие задачки по удалёнке 4 часа в неделю (включая все созвоны), но зарплату получаешь на постоянке.
=
Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но скоро будет мощный третий гайд по SOLID, и дружелюбные цены вырастут:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
=
Новые материалы для ментатов Лаборатории.
В раздел "Элитный программист" добавлен материал
69) Шиза для программиста - 3.
База для тех, у кого проблемы с внимательностью к коду и его логике.
В курс карьеры добавлен 101-й материал "Софт-скиллы или хард-скиллы?".
Это вечный вопрос, и на него есть однозначный ответ.
=
"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.
Гайд по "Calculus of Inductive Constructions",
этим летом 💯 будет готов.
(я решил сперва сделать λ-куб Барендрегта)
=
Трек "Чистое Проектирование/Software Design in Large", материал "Ясная архитектура"
Добавлены все планировавшиеся архитектуры 16-22:
Stream Processing, две расширенных архитектуры на монадах состояний с обработкой ошибок и абсолютной безопасностью, интерпретатор AST, пишем DSL, абстрактный тип данных.
На неделе оформлю в дополнение к действующему материалу ЯА, кто из ныне действующих ментатов в 2025-м ранее изучал, можете бесплатно допройти.
=
Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 20 уровней из ~50 альфа-версии,
переделал на BigInteger, добавил много ачивок и мотивирующих бонусов за различные схемы делания помидорок,
этим летом бета-версия 💯 будет готова.
20-й лвл:
Проникновение в ядро городской операционной системы (Центр Управления Мегаполисом) или его критически важные модули. Кража шифровальных ключей; доступ к архивам всех городских систем; внедрение постоянных бэкдоров; тотальный мониторинг инфраструктуры; попытка перезагрузки секторов.
Мой чип — украденный прототип ЦЕРНа. Ломает банковские SSL за 0.3 нс.
Облако драгоценностей за неделю.
Набор ментатов в Лабораторию на 2025-й год закончен.
(регулярно думаю о том, как становиться меньше и постепенно исчезать из Сети)
Основной паблик:
Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).
Засада с микросервисами
Предыдущие серии:
Засада с исключениями
Засада с инициализацией
Засада с контроллером
Для донов-начинающих:
...Вопрос уже не о том, заменит ли нас искусственный интеллект, а в том, кто быстрее всего освоит искусственный интеллект своих целях. И одна из недооценённых областей интересов, о которой, как мне кажется, говорят недостаточно — это ОБРАЗОВАНИЕ.
6 рекомендаций + промпты для начинающих и всех желающих продуктивно самообучаться.
...Такой простой подход за короткое время -- месяцы, а может даже и недели -- далеко продвинет вас в IT в эпоху AI. Большинство разработчиков до сих пор понятия не имеют об огромных преимуществах использования искусственного интеллекта.
Для донов-неначинающих:
СильныеИдеи++
42. SOLID25 : [2...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.
Продолжение трека "Элитный программист":
29) Как соцсети помогут вам в создании личного бренда.
Вы можете быть элитным программистом с отличными навыками общения и работы в команде, но если ваши публичные профили в соцсетях выглядят плохо, никто не захочет брать вас на работу...
Золотые правила карьеры разработчика.
1. [...]. Идеальный вариант, когда тратишь на рабочие задачки по удалёнке 4 часа в неделю (включая все созвоны), но зарплату получаешь на постоянке.
=
Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но скоро будет мощный третий гайд по SOLID, и дружелюбные цены вырастут:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
=
Новые материалы для ментатов Лаборатории.
В раздел "Элитный программист" добавлен материал
69) Шиза для программиста - 3.
База для тех, у кого проблемы с внимательностью к коду и его логике.
В курс карьеры добавлен 101-й материал "Софт-скиллы или хард-скиллы?".
Это вечный вопрос, и на него есть однозначный ответ.
=
"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.
Гайд по "Calculus of Inductive Constructions",
этим летом 💯 будет готов.
(я решил сперва сделать λ-куб Барендрегта)
=
Трек "Чистое Проектирование/Software Design in Large", материал "Ясная архитектура"
Добавлены все планировавшиеся архитектуры 16-22:
Stream Processing, две расширенных архитектуры на монадах состояний с обработкой ошибок и абсолютной безопасностью, интерпретатор AST, пишем DSL, абстрактный тип данных.
На неделе оформлю в дополнение к действующему материалу ЯА, кто из ныне действующих ментатов в 2025-м ранее изучал, можете бесплатно допройти.
=
Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 20 уровней из ~50 альфа-версии,
переделал на BigInteger, добавил много ачивок и мотивирующих бонусов за различные схемы делания помидорок,
этим летом бета-версия 💯 будет готова.
20-й лвл:
Проникновение в ядро городской операционной системы (Центр Управления Мегаполисом) или его критически важные модули. Кража шифровальных ключей; доступ к архивам всех городских систем; внедрение постоянных бэкдоров; тотальный мониторинг инфраструктуры; попытка перезагрузки секторов.
Мой чип — украденный прототип ЦЕРНа. Ломает банковские SSL за 0.3 нс.
2😁29🔥23👍7❤5✍3
Немного поигрался с лямбда-кубом Барендрегта, пошёл сверху вниз:
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.
Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.
С другой стороны и хорошо что не вышло, всё равно этот куб на практике не актуален, а CoC и HoTT я реализовал, и куда важнее кубическую теорию дальше (успеть) сделать -- чётко под задачи программиста-миддла. Хотя бы научить рассуждать in small в соответствующих моделях. Например, цепочка конвертации данных с помощью унивалентности (композиция путей соответствует композиции эквивалентностей) с автоматическим доказательством коммутативности преобразований. И постепенно выходим на уровень формального мышления in large.
А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....
все уснули давно
в километрах глубин
никого ничего он остался один....
кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...
я сумею доплыть
под сияние звёзд
я хочу увидать край где много берёз...
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.
Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.
С другой стороны и хорошо что не вышло, всё равно этот куб на практике не актуален, а CoC и HoTT я реализовал, и куда важнее кубическую теорию дальше (успеть) сделать -- чётко под задачи программиста-миддла. Хотя бы научить рассуждать in small в соответствующих моделях. Например, цепочка конвертации данных с помощью унивалентности (композиция путей соответствует композиции эквивалентностей) с автоматическим доказательством коммутативности преобразований. И постепенно выходим на уровень формального мышления in large.
А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....
все уснули давно
в километрах глубин
никого ничего он остался один....
кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...
я сумею доплыть
под сияние звёзд
я хочу увидать край где много берёз...
4👍53❤🔥9✍4😁4🤔2
Преподы мехмата рассказывают, что студенты там сходят с ума по нейронкам, хорошо ещё что по математике внутрянки, но всё равно на выходе 98% это говнопроекты с вайб-кодингом, от которых больше вреда чем пользы, и зарплаты так себе.
А вот на формальные темы, верификацию, теорию типов, студента и на аркане не затащишь, хотя это абсолютно критичные темы для тех самых 2% критически важных инфраструктур.
...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.
При этом я даже лично знаю несколько человек, теперь уже полностью "с противоположной стороны баррикад", кто их старательно и успешно к себе сманивает.
Ну и изучают они соответственно западные теорем-пруверы вроде Rocq и англоязычные гайды, и ни о каком развитии этой темки в России конечно речь уже давно не идёт, это я как-то ещё шевелюсь...
...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.
А вот на формальные темы, верификацию, теорию типов, студента и на аркане не затащишь, хотя это абсолютно критичные темы для тех самых 2% критически важных инфраструктур.
...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.
При этом я даже лично знаю несколько человек, теперь уже полностью "с противоположной стороны баррикад", кто их старательно и успешно к себе сманивает.
Ну и изучают они соответственно западные теорем-пруверы вроде Rocq и англоязычные гайды, и ни о каком развитии этой темки в России конечно речь уже давно не идёт, это я как-то ещё шевелюсь...
...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.
2👍53🤔11💯8🔥3😁2
Прекрасное: разработка, управляемая мазохизмом.
A masochist’s guide to web development
Пишем веб-приложение на сишечке и wasm.
emnoscripten, колбеки между си/js, многопоточность в браузере, persistent storage через idbfs... Элегантная фишка: вынос тяжёлых вычислений в веб-воркер.
A masochist’s guide to web development
Пишем веб-приложение на сишечке и wasm.
emnoscripten, колбеки между си/js, многопоточность в браузере, persistent storage через idbfs... Элегантная фишка: вынос тяжёлых вычислений в веб-воркер.
👍34😁19✍10🎉1🤓1
2. Однажды Бобрик пришёл к старому БоброМудру и спросил:
-- Учитель! А если бы появилась теория типов ещё более сложная, чем HoTT и CoC, вы бы смогли и её реализовать?
-- Без проблем, - ответил БоброМудр.
-- Но как?? - изумился Бобрик.
-- А вот так! - ответил БоброМудр, и дал Бобрику подзатыльник.
-- Учитель! А если бы появилась теория типов ещё более сложная, чем HoTT и CoC, вы бы смогли и её реализовать?
-- Без проблем, - ответил БоброМудр.
-- Но как?? - изумился Бобрик.
-- А вот так! - ответил БоброМудр, и дал Бобрику подзатыльник.
1😁62🫡2🤯1
Вчера решил обновить Нах, кнопочкой (сам он не умеет проверять апдейты), и он скачивает и запускает из самого себя полностью автономный инсталлятор. Окошечко с кнопкой скачивания, выбор каталога, весь UI -- какой-то древний стиль Delphi из 2000-х.
Так как инсталлятор автономный то он по определению не способен выбрать каталог установки, где уже размещается Нах; предлагает стандартный c: program files, тоже приходится ручками задавать,
И после чего это чудо ничтоже сумняшеся начинает установку при непосредственно работающем экземпляре Наха, ну и естественно возникает классическая проблема ↑↑↑
(Сделать инсталлятор, автоматически определяющий обновления и умеющий полноценно перезаписывать свою копию при новом апдейте -- это уровень лабораторной работы первого курса на пару часов.)
Детский сад какой-то, ей-богу.
За $1m мои ментаты сделают абсолютно защищённый и формально верифицированный мессенджер уровня телеграма (чаты + продвинутая ai-система рекомендации каналов) на 100 млн пользователей и миллион rps.
Но это в теории, на практике никому не рекомендую связываться с госконтрактами: по итогу сами останетесь много должны, и будете ещё благодарить что не упрятали в кутузку.
Уж лучше, честное слово, чем браться за что-то подобное, лучше заниматься иллюзорным стартаперством =>
"...Последние 3 недели был в Долине: полсотни встреч с стартапами и фондами, организация двух конференций, участие в пяти, два хакатона и куча эмоций.
...В городе не осталось ни одного билборда, который бы рекламировал что-то кроме ИИ. Энергия через край. Я уже писал, что в воскресенье вечером в кафе нет свободного стула, потому что все кодят стартапы. Уровень общего воодушевления выше, чем когда-либо на моей памяти."
А на моей памяти практически точно такое же было в конце девяностых, когда только зарождался тот самый "пузырь доткомов", а потом в 2000-е "пузырь shareware" и т.д. Тогда просто не было доступных ноутбуков, поэтому сидели все за домашними компами 🤓
Так как инсталлятор автономный то он по определению не способен выбрать каталог установки, где уже размещается Нах; предлагает стандартный c: program files, тоже приходится ручками задавать,
И после чего это чудо ничтоже сумняшеся начинает установку при непосредственно работающем экземпляре Наха, ну и естественно возникает классическая проблема ↑↑↑
(Сделать инсталлятор, автоматически определяющий обновления и умеющий полноценно перезаписывать свою копию при новом апдейте -- это уровень лабораторной работы первого курса на пару часов.)
Детский сад какой-то, ей-богу.
За $1m мои ментаты сделают абсолютно защищённый и формально верифицированный мессенджер уровня телеграма (чаты + продвинутая ai-система рекомендации каналов) на 100 млн пользователей и миллион rps.
Но это в теории, на практике никому не рекомендую связываться с госконтрактами: по итогу сами останетесь много должны, и будете ещё благодарить что не упрятали в кутузку.
Уж лучше, честное слово, чем браться за что-то подобное, лучше заниматься иллюзорным стартаперством =>
"...Последние 3 недели был в Долине: полсотни встреч с стартапами и фондами, организация двух конференций, участие в пяти, два хакатона и куча эмоций.
...В городе не осталось ни одного билборда, который бы рекламировал что-то кроме ИИ. Энергия через край. Я уже писал, что в воскресенье вечером в кафе нет свободного стула, потому что все кодят стартапы. Уровень общего воодушевления выше, чем когда-либо на моей памяти."
А на моей памяти практически точно такое же было в конце девяностых, когда только зарождался тот самый "пузырь доткомов", а потом в 2000-е "пузырь shareware" и т.д. Тогда просто не было доступных ноутбуков, поэтому сидели все за домашними компами 🤓
👍43😁13💯4🤔3🤓1