С Днём Победы!

Не успел я как следует проснуться, а доставка еды уже заработала! Заказал праздничный стол из kfc. Лифты тоже не тормозили :)

Где-то ближе к 12 прокатился на велике в озон, пункт нормально работает (думаю, по wifi).

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

Ни машин, ни людей на улицах, так классно. Магазины и банкоматы не тестил, но в целом кстати большой ? : если бы мобильный интернет отключился не официально, а наоборот? Почему вдруг в такой ситуации перестают работать приёмы оплаты в магазинах? Конечно, любые кассы должны уметь работать как минимум оффлайн, кэшируя данные (как, собственно, это было всегда). И почему они не переключаются, например, на wifi или проводной интернет? Это же и к банкоматам относится. Они ведь не на улицах стоят, а в тэцэ и всяческих офисных заведениях.

Паникёр: "Сервер упал! Что делать?!"
Айтишник: "Ничего. Он всегда так делает в пятницу в 5 вечера."

Я закончил курс "Вайб-проектирование с AI"
(он занял примерно на порядок больше времени чем я предполагал :)

Разбираем тему проектирования при использовании AI. Создаём AI-чат на заданную тему ("персональный мотиватор" с использованием локальной модели или внешнего API) с полного нуля, делая основной акцент на правильном процессе анализа требований и Software/System Design. Практически полностью приведено всё общение с Claude 3.7 и весь код.

Для прохождения курса ничего особенного дополнительно не потребуется,
достаточно локально поставить python + pytorch + transformers + gradio (никаких AI IDE).

Уровень скорее для AI-начинающих -- кто общался с LLM в простом чате, получал от него какие-то кусочки кода и имеет минимальное представление, насколько при таком подходе всё получается печально и как быстро всё запутывается :)
Поэтому на курсе ключевой акцент делаем на Programming in Large.
Ну и для всех тех, кто хочет запустить AI-сервис, но не знает, с чего начать.

22 топика:

БАЗА: Рабочий процесс vibe-кодинга
Рабочий процесс vibe-кодинга: база
1) Мозговой штурм и планирование
2) System Design
2) System Design - 2
2) System Design - 3
Технические шаги
3) Скаффолдинг и спецификации кода
4) Генерация кода в середине цикла
Локальная загрузка модели
Программируем чат с моделью
Генерация генератора промптов
Запускаем сервер
Делаем архитектурную ошибку
Спасаем проэкт
Добавляем внешний API
5) Генерация тестов
6) Два основных приёма отладки с AI
7) Рефакторинг
8) Документация
9) Генерация документов
Итоговый результат

Курс доступен только моим курсантам в рамках трека "Ясные Системы"
(рекомендуется после прохождения курса "Ясное BDD").

картинка от курсанта

P.S. Завтра я сделаю важное заявление о дальнейшем развитии Школы.

Дорогие, моя Школа ЗАКРЫВАЕТСЯ. Идите с Богом! :)

А я ухожу
в курьеры на постоянку за млн в финтех в стартап AI-онлифанщиц
в математический ретрит.

Больше в платном доступе "для всех" не будет НИ-ЧЕ-ГО.

=

Бусти со вчерашнего дня ЗАКРЫТ, платной подписки больше нету (в мае для последних подписчиков ещё выложу пару материалов).
Пока остаются для покупки сборники материалов СильныхИдей и ещё 2-3 гайда, но цены уже начали расти на ВСЁ.

=

На новой платформе онлайн-обучения со вчерашнего дня также ЗАКРЫТЫ бывшие доступными всем курсы: по TDD, BDD и лямбда-исчислению.

И в целом, это была моя стратегическая ошибка: намерение делать побольше материалов и курсов "для всех" с автоматическим приёмом оплаты. Само по себе это конечно отдельное неплохое направление, но оно требует существенных инвестиций времени, а результатом фактически будет только одно: деньги. А нафига они мне? Ну, трачу только что умеренно ощутимые суммы на врачей. А так, из одежды например за последние 5 лет я купил только худи "МотоМосква" (не знаете, зачем там шнурочки у капюшона? чтобы их в кофе макать? :).

Хочу не "продавать через механики", а заниматься любимым делом и быть самим собой.

Билл Гейтс вон решил на неделе все свои 200 млрд. долл. просто раздать на благотоворительность... Я правда, ничего не накопил, но на благотворительность много лет ежемесячно доначу в три фонда: фонд "Старость", фонд Хабенского и WorldVita. Мне даже банк предлагал налоговый вычет за эти донаты (которые я хотел обратно в фонды отправить:), но потом замолк.

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

=

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

Оба паблика VK для донов продолжают работать как обычно!
Сегодня не-начинающим выложил базу про паттерн Visitor -- почему это по сути приляпка, компенсирующая качественные недостатки ООП (данные и поведение хранятся вместе по определению, но наследование может легко поломать LSP), и насколько элегантно проблема решается использованием функционального стиля. 35-й материал, а всего их за сотню будет.

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

Но, стоимость подписки новым донам в обоих пабликах в ближайшие дни РЕЗКО вырастет.

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

На видео: это я в ожидании, когда через 30 минут стартует-Джиро 25 закроется моя Школа.

...Далее, полностью сосредотачиваюсь на математике и theoretical computer science. Даже от темок программной инженерии и system design хочу отказаться, и вообще от всего айтишного, где относительно небольшой порог входа — что сегодня может норм пояснить любой ментор с сеньорским опытом или жпт с дипсинком.

В общем, пошёл для начала медитировать, по наводке Алана Кэя, на мета-компилятор Meta II, созданный 60 лет назад для 6-битного компьютера IBM 1401: "A syntax-oriented compiler writing language". Заложенные в него фишечки и по сей день остаются во многом непревзойдёнными и нереализованными.

Его автор Val Schorre придумал крошечную мета-фичу, которая однако сумела сразу охватить семантику широкого спектра языков более высокого уровня ("Math Wins!"). Он также исхитрился применить эту мета-идею к самому мета-компилятору и получить псевдокод для системы, которую смог выполнить простой интерпретатор, запущенный на 1401.

Для разминки, коан: переосмыслить null как "несуществующее даже для самого себя". Согласитесь, и синтаксически и семантически эксплицитное обозначение отсутствия чего-либо в системе, смотрится парадоксально.

Медитирую, соответственно, в мета-направлении "Math Wins!" для современного Software Design, в идеале -- через подобные микро-мета-фишки. Для чего сперва эти мета-фишечки надо смоделировать, в идеале, с помощью гомотопической теории типов. Делаю это всё, конечно, исключительно ДЛЯ ВАС 🙏🙏🙏

❤️ Я буду жить для тебя ❤️

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

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

Апрельские тезисы Алана Кэя, и про первый в мире алгебраический пруф-чекер из 1950-х. Как тебе такое, И.М.?

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

Секретный секрет легендарного миллиардера: как правильное целеполагание забустит вашу продуктивность в космос 🚀 + какую книжечку почитать по теме.

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

СильныеИдеи++
35. Ключевой паттерн Visitor в ООП и ФП
Разбираем примеры Visitor в ООП и ФП, рассматриваем плюсы и минусы каждого, смотрим multiple dispatch, mixins и т.д.

Продолжение трека "Элитный программист"
26. Автоматизация создания хорошей эхо-камеры .
Если присутствие того или иного контакта в списке друзей не приносит вам никакой пользы, стоит подумать о его удалении. Помимо того, что это способствует удалению неактуального контента, который вам показывает бесконечная лента, удаление определённых людей из списка контактов имеет и другие преимущества...

Завтра цена подписки для новых донов сильно вырастет.

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

Бусти: закрыт.

Курс "Гомотопическая теория типов для малышей программистов: ТОП (Топологически Ориентированное Программирование)".
"После майских" курс 💯 будет готов. С сегодняшнего дня ре-активирован 🚀
К лету курс 💯будет готов.

Курс "Ясные Системы" (как быстро и легко писать ПРОСТОЙ код систем масштаба ultra-large-scale).
пока 28 эвристик, как наберётся 42, дам курсантам доступ.
Отложен на будущее (которое не настоящее).

Курс "Ясное AI"
"После майских" курс 💯 будет ГОТОВ.

Просили пояснить за ТОП: что с этого будет ровным пацанам?

ТОП - это когда мы не просто высокоуровневые спецификации (полученные например с помощью BDD) переводим в некоторый код (как сегодня фактически происходит во всём мировом программировании, от вайб-кодинга с околонуля до монадических механик на этих ваших хаскелях),

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

Но главное, что мы таким образом задаём и правила композиции этих путей, что позволит проектировать логику системы как когерентное взаимодействие слоёв абстракций.

Модульность — через унивалентность (эквивалентность изоморфных структур).
Управление потоком вычислений -- через зависимые типы (как спецификации инвариантов).
Композиция эффектов — через transport along Path (согласованное преобразование контекстов): "переносим" значение из типа A в тип B с сохранением внутренней структуры, если задан путь (доказательство тождества) p : A = B.
Говоря по-программистски, гарантированно безопасное приведение типов.
Сложная логика — через высшие индуктивные типы (инкапсуляция состояний и переходов).

Например, тип List задаёт свободную алгебру над сигнатурой {nil, cons}, а его элиминатор -- рекурсивную схему, логически ограничивая допустимые операции.

Тип (как спецификация пути в ∞-группоиде вычислений) по сути автоматически "выбирает" код своей реализации!

=

Вообще, транспорт через тождества из HoTT (слоистая композиция через когерентные гомотопии, ну или аналог рефакторинга с гарантиями — как вам больше нравится :) -- это прям мощща (монадические bind + pure/return ушли курить далеко и надолго).
Гарантируем, что "побочные эффекты" не нарушают глобальную структуру (на уровне зависимых типов -- например, List -> Vector для конкретной длины).
А сами завтипчики (с продвинутым паттерн-матчингом) позволяют статически кодировать пред- и пост-условия (логика как доказательства), а унивалентность позволяет сменять реализации, сохраняя эквивалентность.

Короче говоря, тип f : (x : A) → B(x) в HoTT -- это не просто функция, а доказательство, что для любого x в A существует конструктивный метод получения B(x), встроенный в целостную гомотопическую структуру типов нашей системы.

Таким образом, подобная система типов становится метаязыком (MetaDSL a-la Math Wins по Алану Кэю) для проектирования логики, где программы -- это не наборы инструкций, а доказательно-топологические конструкции, формально управляемые правилами HoTT.

=

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

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

=

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

"К лету курс 💯будет готов."

Предварительный уровень? Ну вот кто прошёл успешно мои курсы "функциональное программирование на F#" и "солвер Z3 на Python", значит готов на 💯

...И в то же время, хотя это всё может дать невероятную продуктивность - десятки, сотни раз! -- этим практически никто не занимается. Даже не математика и tcs, а достаточно рядовые достижения cs и программной инженерии.
Никому особо это не нужно, как неуловимый Джо. Парадокс?

А вы спросите у своего техдира, сколько он готов заплатить за услугу, которая гарантированно ускорит выпуск фич например в 42 раза. Команда 3-5 программистов (условный миллион зп в месяц на всех), что могла сделать за год, сделает за 1 неделю. Экономия получается более 11 млн. рублей, казалось бы, да? А заплатить надо, допустим, 1 миллион. Вроде бы надо мгновенно хвататься за такой шанс всеми тремя руками, правда? (и мы даже вопрос недоверия исключим: допустим, есть хороший набор проверенных отзывов от известных компаний, гарантия возврата денег и сохранения всех рабочих процессов as is...).

Ага, щас. CTO CEO будет скрежетать зубами, лишь бы не заплатить даже тыщу долларов за ускорение работы над проектом в сотню раз, и даже "попробовать бесплатно" не сработает. Это ведь в некотором смысле будет признанием своей эээ не совсем полной профессиональной пригодности.

Животные будут с оскаленными клыками охранять свою территорию до последнего:)

Вот есть типичная ситуация с техдолгом "в нашем бэклоге задач на 10 лет вперёд". Вы думаете, тимлид обрадуется предложению "в вашем бэклоге задач на 10 лет вперёд, а через месяц задач останется на один год"?

Да нифига. 98% наёмных менеджеров заинтересованы в максимальном затягивании сроков "по объективным причинам". И даже если удастся договориться с владельцем бизнеса (которые, что (не)удивительно, тоже весьма редко настроены на такие продуктивные изменения, едва дело касается практических телодвижений), на всех остальных уровнях встретится тотальное сопротивление. Потому что и сами разработчики этого совершенно не хотят, для них это просто очередное усиление эксплуатации.

Вот вы начали использовать AI, стали делать тикеты реально во многие разы быстрее, ну и? Выросла ли при этом ваша зарплата хотя бы на 50%? Да хотя бы на 10%?
ФИГ!

"Мы Вы рабы ничего не стоящие, потому что сделали, что должны были сделать"
Лука 17:10

Потому что менеджеры особо не понимают ,что вы реально ускорились, да и не придумано пока достаточно объективных метрик измерения роста продуктивности. Сроки берутся с потолка, ну тимлид как-то слегка апроксимирует в голове ваш предыдущий опыт на сроки новых задач, но это очень условно. Ему важнее, чтобы вы гарантированно укладывались в оговорённый срок. А будет ли он 3 дня или месяц, не так существенно на самом деле. И даже если вы сделаете текущую задачку в 10 раз быстрее, и радостно сообщите об этом начальнику, в лучшем случае он напишет вам три буквы "спс". Никогда так не делайте! :) А на что потратить высвобождающееся время, вы знаете.

Поэтому и коммерческих курсов на эти темы не появится: продавать рост продуктивности даже в сто раз практически нереально. Я общался с PhD из MIT, который вложился в мощные курсы по software design для обычных программистов, но практически никто у него не покупает.

Физики платить в основном готовы за "стать фулстек-программистом с нуля за полгода на 256k" или какие-нибудь быстрые курсы повышения квалификации по техническим фреймворкам, которые постоянно в вакансиях пишутся или востребованы на работе, и всё. А юрики -- за корпоративное обучение чему угодно для галочки (с итоговой нулевой эффективностью), но зато с откатом 98%.

Всё остальное остаётся уделом университетов.

Я вообще один уже наверное остался, кто бредёт в сторону, полностью противоположную мэйнстриму...

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

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 в помощь.