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

Делаем такое (с)мутное понимание эксплицитным, что даёт возможность за счёт непрерывного фидбэка его невероятно прокачивать вообще без пределов!!1

Как профессиональный пианист с консерваторским образованием может легко и просто играть любую музыку, так ты после гайдов с практикой на Lean4 сможешь уверенно выстраивать сложнейшие композиции паттернов/абстракций в любом языке, где есть минимальная поддержка функционального стиля (Python, C#, Java, PHP :).

Что имею в виду: джун в голове может удерживать одновременно 2-3 абстракции, может их скомпозировать на 1-2 уровня, а о том, что есть математические правила композиции, даже и не знает (ну, если только не занимался в моей Лаборатории :). На отладку такой композиции тратит до 8 часов.

Миддл: 4-7 абстракций, 3-4 уровня композиции. Знает, что есть какие-то правила, но не всегда помнит, какие именно подойдут в той или иной ситуации. На создание/отладку - 4 часа.

Сеньор: 6-9 абстракций, 4-7 уровней композиции. Понимание законов: 30-50% (знает основные, интуитивно применяет). В основном методом проб и ошибок, рефакторинг может сломать его художества легко и просто. На создание/отладку - 1.5-2 часа.

Лаборатория: 10-15++ абстракций, 8-10++ уровней композиции. Понимание законов: 90-95% (можешь доказать, почему работает). И создаёшь такое буквально в режиме непрерывного набора текста, за полчаса.

На картинках: максимально простой детский учебный пример, уровень джуна ))) Reader, State и Except.
Спека на лине, и рабочий код на F#.

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

Свежие прогнозы, что к концу текущего десятилетия 90% кода будет писано AI, и думаю, это реально. Главный вопрос, какой процент архитектуры, software design будет приходиться на долю AI :) Полагаю, он будет резко падать по мере роста проекта. 3-5 тысяч строк кода standalone-система - ну возможно, AI потянет архитектуру. Десятки тысяч строк -- уже почти невероятно, сотни тысяч - фактически нет.

В этом плане крайне показательно, что AI (ЖПТ5Кодер) совсем слабенько пишет код на лине. После десятка подсказок еле-еле выдаёт что-то работающее более-менее сложное. А Клод4.5, что удивительно, вообще не тянет, ну совсем практически. Не способны они в принципе мыслить проектными абстракциями :)

Чем мне крайне нравится такой подход? Тем, что он впервые в мире в обучении сложным темкам в проектировании даёт гарантированный критерий правильности решения (за счёт сильной системы типов). Условно говоря, программа либо "компилируется" (доказывается, что она гарантированно правильная), и её можно использовать, либо нет (неработающая).

Я мечтал об этом давно, но вот только сейчас понял, как это сделать. Благодаря Филдсовскому лауреату Теренсу Тао, кстати, инсайт был после его подкаста "Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI" (есть автоматическая озвучка на русском).