Продолжаю работу с курсантами 🤓

Cегодняшнее:

...Недавно у меня была аттестация в компании. Менеджер сказала, что заказчик доволен моей работой, но не готов пока повысить мою ставку, и поэтому компания не может повысить мне зп. Что рассмотрят повышение в июле. Для меня это было неожиданно, и я спросила, а на какое повышение могу в принципе рассчитывать. Менеджер замялась, сказала что не хочет ничего обещать, но возможно 10%.
Вообще, это для меня первый опыт переговоров о повышении, судя по всему, я довольно слабо их провела. К июлю планирую применить рекомендации из "Курса Карьеры", чтобы быть более подготовленной.
...Но есть и плюс, компания одобрила и готова оплатить мне сторонее обучение по архитектуре.

Ситуация кстати довольно типичная: вами во всём довольны, но денег нет "по независящим причинам". На самом деле это враньё: если видят что человеку можно просто не заплатить, то и не заплатят. Но при этом за рост ваших скиллов, чтобы вы работали в разы продуктивнее, они платить готовы :)
Дело не в слабых переговорах, а в отсутствии системного подхода. Эту тему надо регулярно прокачивать, начиная за полгода минимум до аттестации. Как это делать, я подробно разбираю на треке БПЗ.
+10% это конечно вообще ни о чём: если за год зп не вырастает хотя бы на 20-25% (стандарт 2x15%), значит далее будет только хуже.

...Индексацию з/п не проводили с начала СВО. В этом году планировали, разговоров было сверхмного, а в результате выделили три копейки в масштабах всей организации. У нас руководство вообще не поняло, как поделить эти деньги. В результате, увеличили всем оклад на одну тысячу рублей. Очень многие сказали "а, ну хорошо" и сейчас прямо на работе ищут работу.

Майское:

...Вот и последствия длинных выходных)
уже успел забыть происходящее

...За 3 года на работе понял, что заблуждался по поводу прокачки и роста, у меня есколько поменялся взгляд на разработку, некоторые вещи, которые раньше казались важными, перестали таковыми являться сейчас. Через некоторое время я освоился с рабочими задачами и стремительный рост прекратился. Заниматься дальше на других курсах я не стал. Были разные жизненные ситуации, из-за которых очень легко было оправдывать своё бездействие в плане учёбы. Сейчас я понимаю, что так продолжать нельзя, ибо этот путь приведёт на обочину IT-мира. Нужно учиться, чтобы оставаться на плаву и достигать новых высот. С начала этого года решил взять за ум и
Ещё ощутил важность хорошего проектирования. На работе поручили создать новый сервис и я испытывал дискомфорт, от того, что толком не понимал хороша или плоха моя архитектура, как нужно делать, а как – нет.

...задача перевода интеграции на новый движок встряла, и вдруг спустя время перед майскими всем срочно нужно было чтобы она заработала, пришлось 9 дней подряд включая с 1 по 4 мая выяснить как это раньше работало(написал эту интеграцию человек который проработал у нас осенью месяца 3 а потом просто исчез) и как теперь должно работать.

...Сходил на собес к производственнику и попил кофе после тренировки с владельцем небольшой фирмы, которая делает беспилотники. У них типа кадровый голод, готовы платить 250+, но опытным спецам в их стеке (у первого какие-то нейросетки для оптимизации производственных издержек , у другого микроконтроллеры и си / ассемблер).

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

🔥 Мой мидл-лайф на Java & Spring (зумер-версия) 🔥

Прикиньте, я — программист-зумер ☕️ (уже мидл, но в душе джун). Пишу на Java (олдскул, но с вайбом).

Мой стэк:
✔️ Java (80% времени гуглю "как избежать NPE");
✔️ Spring (аннотации — это магия, а @ Autowired — моя религия);
✔️ Hibernate (иногда ленивый, иногда — нет, как мой кодревью).

Как я работаю:
1️⃣ Открываю IntelliJ IDEA (без джетбрейнза — как без души);
2️⃣ Запускаю Spring Boot (жду 5 минут, пока бины протрезвеют);
3️⃣ Пишу код (но сначала спрашиваю у Copilot 🤖);
4️⃣ Ломаю прод (но чиню до того, как тимлид открывает Jira).

Мои эмоции:
✅ Тесты прошли с первого раза? Я — гений 🧠✨;
❌ Упал прод? "Это баг в Spring, не мое" 🐞;
👀 Вижу legacy-код? "Ктоэтонаписал?!" (потом вспоминаю, что это я).

Моя философия:
🔧 Работает? Не трогай.
♻️ Не работает? mvn clean install.
💥 Совсем не работает? Перезапусти IDE.

Вывод:
Я — мидл, но чувствую себя сеньором (пока не спросят про транзакции).

P.S. Если код странный — это не баг, а фича 🚀

#Java #Spring #ZумDev #МидлНаМореКофе

Смешное: как пацан джва года пилил игру на Rust, а потом психанул, и за шесть недель переписал всё на C# и юньку, и наслаждается комфортом.

Причины из материала, по которым Rust не покатил:
- сложность быстрого прототипирования;
- проблемы с обновлениями движка Bevy и API-дрейфом;
- ограниченная поддержка AI-инструментов для Rust.

Rust даёт нам как бы мемори сэйф, но напрочь отнимает безопасность психики :) Шарпик хотя бы оставляет нормальный рассудок. А Unity как старый добрый дедушка: периодически ругается, но хотя бы предсказуем.

Но в целом я однозначно за изучение Rust, если вы пишете на Си/С++, да ещё и работаете в геймдеве, или разрабатываете что-то системного профиля. Сильное подозрение, что жпт ещё долго не будет тянуть Rust, и порог входа в эту тему останется достаточно высоким, что 💯 хорошо в плане нишевых вакансий и продвинутых зарплат.

Сколь бы не были сильными абстракции уровня programming in small

(как я например использовал для демонстрационной игры Змейка -- самые сильные на сегодня в математическом смысле),

толку от них будет абсолютный ноль и вся система мгновенно развалится, достаточно дать совсем немного слабины на уровне programming in large.

Форматирую для курса код Змейки, который нагенерил
"...в полностью агентных задачах лидируют SWE-Agent, Github Copilot (VSCode), Windsurf - почти все на базе нашей любимой Claude 3.7 Sonnet."

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

Глаз зацепляется вот за такое:

def toggle_pause(self, state: GameState, engine) -> GameState:
        engine.toggle_pause()
        return state

WTF??

То есть для галочки AI сделал функцию в чисто функциональном стиле, да вот только логика её оказалось кривейшей глобальной зависимостью.

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

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

Но зато на удивление естественно и продуктивно в вайб-проектирование укладывается мой трек по ООАП: я сейчас рекомендую всем, кто прошёл с него третий курс (делаем проект по предлагаемой методике), перепройти его заново уже в связке с AI и с учётом новых рекомендаций.

=

А главный вывод в том, что, как закончу второй курс по базовой теории HoTT, надо будет думать прежде всего в направлении топологически-ориентированного проектирования: как всю эту могучую силушку гомотопической теории типов залифтить до programming in large.

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

Но это всё остаётся всё же какое-то половинчатое programming in large in small. Можно например попробовать кодировать бизнес-правила и ограничения как "пути" между зависимыми типами...

Пока не знаю, размышления продолжаю.

Существуют парадигмы, и парадигмы на ранних этапах разработки программного обеспечения очень помогли нам. Например, структурное программирование намного лучше, чем goto, это здорово, это действительно сэкономило нам много времени...
но большая часть работы, которой все занимаются целый день, не имеет ничего общего с парадигмами программирования, и точка.
-- Фредерик Брукс

Хвалёный дипсик с дипсинком не смог асилить 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.