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

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

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

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

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

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

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

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

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

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

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


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

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

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


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

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

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

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

=

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

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

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

=

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

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

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

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

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

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

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

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

=

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

=

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

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

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

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

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

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

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

=

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

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

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

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

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

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

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

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

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

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

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

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

=

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

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

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

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

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

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

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

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

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

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

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

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

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

Относительно мышления на условном уровне проектирования/ programming in large, всё что Terence Tao упоминает -- это сплошные эвристики. В проекте Lean4-Analysis-Tao Тао много занимался глубокой медитацией мысленными экспериментами-"симуляциями", чтобы определить, какие леммы нужны для доказательства сходимости рядов. По его словам, он мысленно проигрывал в голове возможные пути доказательства, выделяя ключевые шаги.

(Попробуйте-ка попросить своего менеджера выделить вам время на обдумывание структуры проекта -- в виде например "гулять по парку" или "сидеть в уличном кафе в медитации за чашечкой кофэ" :)

Интересно что Тао использовал подходы к декомпозиции, характерные сегодня для нейросеток: "Decompose-ToM: Enhancing Theory of Mind Reasoning in Large Language Models through Simulation and Task Decomposition"

=

И снова и снова Тао повторяет мантру, что процесс выделения лемм — это искусство, а не алгоритм. Дескать,
- контекстная зависимость
- нет универсальных правил для выбора лемм
- математик часто опирается на неявные знания и аналогии, которые сложно выразить в виде формальных шагов
- cлишком мелкие леммы усложняют общую структуру, слишком крупные - теряют ценность для повторного использования.

Тао подчеркивает, что декомпозиция — это не столько технический метод, сколь "думательная/мыслительная дисциплина". Он рекомендует применять SOLID
- начинать с простых аналогий (например, разбить доказательство теоремы Пифагора на 3-4 леммы);
- использовать пруф-ассистенты вроде Lean для визуализации связей между леммами;
- избегать чрезмерной детализации: леммы должны быть достаточно общими для повторного использования.
Лемма должна решать одну конкретную подзадачу, которая повторяется или критически важна для доказательства (SRP).
Леммы формулируются так, чтобы их можно было применять в разных контекстах.
Если промежуточная теорема требует многошагового доказательства, её разбивают на леммы. И т.д.

Ничего не напоминает? :)

Леммы — "библиотечные функции": однажды доказанные, они применяются в новых теоремах. Функции легко и просто вызываются в разных контекстах, если соблюдаются их контракты. и т.п.

Всё это фактически украдено, причём в весьма лайтовой версии, у программной инженерии, cтабильно рекомендующей это всё последние лет 50 с гаком.
В формализации PFR например леммы были организованы как модули с интерфейсами в Lean.

Математики, что с лицом? :)

=

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

Ну и зачем нам изоморфизм к этой никакой не математике, а по сути, чистой инженерии с эвристиками?

В айтишке это всё работает давно и на порядок качественнее и продуктивнее.

(потерпите, немного додумать осталось :)

...В принципе, для этого всего можно найти много близких аналогий: категорная дуальность (леммы -- это морфизмы в категории доказательств, функции -- морфизмы в категории типов), абстрактная интерпретация (доказательства - типа, спецификации; функции - типа, их реализации), Карри-Ховард конечно классика — да только нафига.

Как не было толку от хаскелеподобных подходов, так и нету, разве что совсем нишевые ниши вроде формальной верификации (например, из Lean в Rust), документирования кода через "контракты" (как в Eiffel/Dafny), ну и обучение конечно.
Для практики нужен язык как минимум с поддержкой зависимых типов, и чтобы он был распространён хотя бы как F#.

=

Короче говоря, резюме такое, что даже самая топовая на сегодня математика уровня филдсовских лауреатов пока что только-только пытается выбраться из детсадовских штанишек programming in small. Забавно смотреть, как математики изобретают велосипед, открывая для себя например гитхаб, где леммы распределялись между участниками как issues, с PR, а их доказательства проверялись через CI/CD )))

Взять нам у них нечего, а вот дать можем очень много.

=

Соответственно итоговая цель получается такая, что вместо утверждений Тао, по сути, по теме programming in large, что

- процесс выделения лемм (классов, функций) — это искусство
- декомпозиция — это не столько технический метод, сколь "думательная дисциплина"

мы должны получить такую базу:

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

Думаю, что тут пока вполне можно остановиться на ООАП по Бертрану Мейеру, усиленному моделью акторов по Алану Кэю и Карлу Хьюитту, и получить очень хороший практический результат. Для начала, первый шаг -- отшлифовать немного мой трек ООАП теоркатом, GADT и HoTT.

Закроем сейчас programming in small гомотопическими типами, и возьмёмся за финальную темку в программировании :)

Нейросетки в модели акторов, да и вообще в асинхронщине, тупят очень жёстко. Пробовал несколько самых последних, вот например Клод 3.7 MAX быстро начал проситься обратно на синхронный формат:

...Ошибка указывает на то, что актор GameEngineActor был остановлен до того, как смог обработать сообщение. Это может происходить по нескольким причинам:
1. Актор мог завершить свою работу из-за необработанного исключения внутри его методов
2. Другой код мог явно остановить актор раньше времени
3. Возможен конфликт при инициализации акторов
Для решения этой проблемы рекомендую следующие шаги:
[... бла бла бла добавить логирование и обработку исключений ...]
Если проблема не решится, можно временно отказаться от модели акторов и вернуться к синхронной обработке для отладки: ...

Ну так ты же сам этот код и написал, вот и разбирайся в причинах :)

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

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

Как даже хорошо подобранные обучающие примеры помогут в условном "обобщении" этих тем для AI в реальных проектах, не представляю.

Пока одни занимаются вайб-кодингом, другие оптимизируют микросекунды ручного набора кода в vim-е, плагин hardtime.nvim в помощь 💪🏻

SaaS is Dead.

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

Чем острее некоторая компания нуждается в вашем SaaS-инструменте, тем более эээ своеобразным будет их Big Ball of Mud (попросту говоря, здоровенная куча устаревшего говнокода), и тем более эээ неожиданными и нестандартными (попросту говоря, откровенно дерьмовыми) будут их рабочие процессы.

Вы потратите сотни часов на поддержку этих "уникальных" случаев, чтобы получить убедительные саксесс стори, и при этом 98% таких случаев не приведут к покупке SaaS-подписки.

Невероятно велика пропасть между "Похоже, это действительно классная идея, надо запилить СааС!" и "Кто-то реально собирается потратить время и ресурсы на внедрение этого сервиса в свои воркфлоу."

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

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

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

Вы же помните, как Пончик в НнЛ создал свой стартап по продаже соли, пока об этом не прознали корпорации? Хорошо ещё, что в кутузку в итоге не попал.

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

Кодекс-l и Опус-4 за 200 долларов я тестить не планирую, ну и как бы то что он "думает часами над задачей и рефакторингом" отнюдь не плюс в его пользу, а здоровенный минус. По полдня ждать его результатов... Это сколько же гигабайтов кода он сгенерит или перелопатит за такое время с абсолютно непредсказуемыми последствиями 🤡

В AI сегодня ценен именно реайлайм в плане фидбека.

=

А Клоду 4 я дал простую задачку: сделать консольную Змейку в модели акторов. Сперва он затупил с версией pykka, сделал на каком-то старье 3.x, которое давно задепрекачено (при том что конечно менять API популярной библиотеки западло само по себе).

Потом Клод стал доказывать, что он такой бедный несчастный обучен на данных 24-го года и не в курсе про новую версию, а в гугле забанен ☠️ после чего я потыкал его мордой в собственные какашки 💩 => версия пукки 4.0 вышла ещё в 23-м году. Он извинился и выдал нагора 330 строк кода, которые вроде бы запустились норм.

Но потом Змейка стала просто случайно завершаться (не вылетать). Я даже на асинхронщину не стал грешить, а просто повнимательнее посмотрел код, и оказалось, что в одном месте (в середине файла) размер игрового поля тупо захардкожен 🤮 20 x 17, а в другом месте, где рендер, используется 22 x 19 🙈

Я попросил это пофиксить, сделать норм с константами, после чего Клод 4 зачем-то решил "улучшить код в целом", и в результате вообще сломал,

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

...А потом я забылся и случайно зашёл через бесплатный голландский впн (Клоду сервер нужен только США), и антропик меня забанил 👊

Но честно сделал рефанд за месяц 22 евро 💰на эстонскую карточку.

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

Когда-то был классный хвост-провайдер Zenon, я на нём одном лет 20 держался, всегда стабильный, всегда быстрая техподдержка по телефону и почте. Помню, как в 2022-м ддосили какой-то наш крупный СМИ-сайт, и мой крохотный учебный сервис случайно оказался с ним на одной виртуалке и стал ощутимо тормозить. И вот пацанчик в разговоре по телефону в реалтайме глянул в чём траблы, перебросил меня за одну минуту на другую машину, и всё заработало норм.

...А в том году его купила, более крупная рыба, понятно что и техподдержка тоже была объединена. И вот всё утро админ забухал сайт skillsmart.ru со всеми учебными серверами лежит, по телефону просто сказали "ой пишите запрос из лк", на сервере уже давно 504 Gateway Time-out, и никакой реакции.

Впрочем, совершенно не удивлён и дальше будет только хуже.
Graviora manent.

Если вы набираете команду качественных разработчиков на серьёзный проект, то наличие у кандидата LLM-подписки - это красный флаг. ⛔️

Ого.

Is the Y Combinator 3rd order / in lambda calculus ?

Клод 3.7 =>
Yes, the Y Combinator is indeed a third-order function in lambda calculus.
...

Клод 4, Опус 4 =>
The Y combinator is not 3rd order - it's actually a 2nd order function (also called a higher-order function).
Y = λf.(λx.f (x x)) (λx.f (x x))
The Y combinator is a 2nd order function that enables recursion in lambda calculus by finding fixed points of functions. It's one of the most famous examples of a 2nd order function, but it doesn't reach the 3rd order level since it doesn't manipulate other higher-order functions.

-- Y can work with different orders
factorial :: (Int -> Int) -> Int -> Int  -- 2nd order input
factorial f n = if n == 0 then 1 else n * f (n-1)
higherOrder :: ((Int -> Int) -> Int -> Int) -> (Int -> Int) -> Int -> Int  -- 3rd order input

Abstracted type is 2nd-order: When we look at Y's type signature abstractly:
Y :: (a -> a) -> a
This type itself is 2nd-order.

So you're correct that while Y's abstracted type signature is 2nd-order, its behavior is order-polymorphic - it can operate uniformly across different function orders due to the polymorphic type variable a.

Я полностью закончил (сделал в смысле :) первый в мире (почему первый в мире? потому что он никому особо не нужен :) курс "Гомотопическая теория типов для программистов (1)", о котором мечтал лет 10-15 назад в духе "эх, вот бы такой когда-нибудь просто закончить (пройти в смысле:)!". Силлабус выложу для курсантов, ну вкратце - интуиционистская версия HoTT, отличия от MLTT, топологическое пространство, гомотопическая эквивалентность, Sum/Product-типы, Path, HIT, n-мерный тор, зависимые Пи-типы и Сигма-типы -- реализуем это всё на Python, все исходники + в тестах разбираем основные use cases, и в заключение делаем на этой базе игру Змейка.

Вторая часть конечно обязательно нужна для полноты (∞-группоиды, гомотопические группы, иерархия универсумов, эквивалентность типов, унивалентность...), но там уже в некотором смысле будет попроще, если проходите, первого HoTT-босса :)

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

Самый важный мета-результат, что в процессе я получил правильные инсайты :)

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

Даже самые сильные на сегодня математические абстракции для программистов -- это всё уровень programming in small, максимум programming in large in small. Хотя, безусловно, закрыть теоретически programming in small само по себе неплохой результат.

...А вот в теме programming in large (тем паче в ultra-large-scale) ничего более-менее формального и близко нету вообще. И я теперь не уверен, нужно ли оно там в принципе, или лучше наоборот перейти на светлую(?) сторону программной инженерии? Главное, с одной стороны, соблюдать разумный формализм, но с другой стороны -- не давать клювику хотя бы даже капельку увязнуть в системной инженерии (когда мы заходим через онтологию, как в каком-нибудь фреймворке Захмана). Даже BDD будет пожалуй слегка перебором.

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

=

Пойду в парк думать, медитировать и слушать Нильса Фрама. Он исполняет на гениальном инженерном произведении Klavins M450 (строгое ч/б пианино высотой 4,5 метра(!). Открытые струны, ручная работа, весит почти тонну (концертный рояль Steinway D в сравнении с ним пушинка 500 кг).

"Nils Frahm - Wesen (Official Audio)"

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

Как в нынешнее время удержаться на работе, чтобы стать незаменимым, и вместо тебя не взяли AI-кодера?

1. Пихайте микросервисы куда только можно, особенно в ключевые модули. Они там бесконечно тухнут, постоянно отравляя проект, но в прогнившем виде будут стабильно тянуться из версии в версию через любые рефакторинги, оставаясь живее всех живых, и никакой AI их не заборет.

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

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

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

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

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


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

И всё же, людей, которые сегодня учатся программировать исключительно с помощью искусственного интеллекта и LLM, ждет неприятное пробуждение в реальность...


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


37. Жёсткий хейт SOLID | OCP (СильныеИдеи++)
Open-Closed Principle - идея, что код должен быть открыт для расширения (т. е. его функциональность можно неким магическим способом расширить без его изменения), и закрыт для внесения изменений (т. е. вы можете доверять тому, что он делает, поэтому вам не нужно дополнительно возиться с ним). Честно говоря, сегодня уже мало кто понимает этот принцип, потому что он был мудрым советом лет 30 назад :)


Продолжение трека "Элитный программист":
27) Отработка "мягких" навыков в безопасной среде.
Участие в качественных технологических группах в соцсетях может помочь вам и в развитии "мягких" навыков. Ведь многие из них связаны с общением, как происходит в большинстве групп.
Вот некоторые из приёмов, которые можно использовать ...

20.05.25. Набор в мою Школу (3 места закончились за 4 минуты).


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


+ Курс "Гомотопическая теория типов для программистов(1)".
"После майских" курс 💯 будет готов.
К лету курс 💯 будет готов.

2025 план стартапа: бросить школу и создать API/SaaS оболочку для ЖПТ.

Почему Spring мёртв?

Потому что есть опенсорсный Quarkus
(Supersonic Subatomic Java)

A Kubernetes Native Java stack tailored for OpenJDK HotSpot and GraalVM, crafted from the best of breed Java libraries and standards.
(пацаны из red hat, зашлите сотку баксов за ad)

Смерть от жадности
Spring Boot жрёт память как голодный монстр — 4 ГБ против 400 МБ у Quarkus. Платишь за воздух!

Старт как у динозавра
45 секунд на запуск? В эпоху облаков это как ждать Windows 95. Quarkus — 0.3 секунды и ты в деле!

Реактивность или смерть
Spring топит треды, Quarkus летает на ивент-лупе. Ты всё ещё в каменном веке с блокирующим I/O?

Конфиги-зомби
50 строк настроек против 6. Spring Boot превращает твой код в помойку — Quarkus даёт чистый код и свободу!

Тесты-черепахи
Spring Boot тесты ползут, как улитки. Quarkus — ракета: горячая перезагрузка за 0.2 сек и тесты на стероидах!

Облака тебя сожрут
Холодный старт Spring — 45 секунд. В serverless это как приехать на такси после того, как вечеринка закончилась.

Кошелёк плачет
65% экономии на инфраструктуре с Quarkus. Spring Boot — это спуск денег в унитаз под видом "надёжности".