Закачиваю гайд по Calculus of Constructions, много читаю по теме, вот свежачок "Programs as Singularities" университета Мельбурна.

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

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

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

Авторы предлагают т.н. "структурный байесианизм".

Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.

Таким образом формируется математический мост между классическим программированием и машинным обучением.

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

Например, алгоритм сортировки может быть представлен как зависимый тип
Sort : (A: Type) → (List A) → (List A) с доказательством упорядоченности, а нейросеть можно представить как тип NeuralNet : (Input: Type) → (Output: Type) → Type

Определяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.

Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.

Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)

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

Основная проблема сейчас -- это исключительно разрыв между теоретической красотой HoTT и практическими инструментами для её применения в реальных задачах (такими, как у меня, но "я их вам не отдам, потому что у меня велосипеда нету" (с) Печкин :). Можно пытаться использовать кривейшие европейские теорем-пруверы, но у нас это зашквар, да и прошлый век уже.

Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.

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

Во-вторых, если серьёзно, на самом деле вы программируете на чистом функциональном языке препроцессора cpp (не путаем с c++ конечно), который состоит только из nestable expressions, которые не выполняются а оцениваются, и yields чистое значение типа Си, которое есть абстрактный тип данных (реализованный как char*). Затем это значение типа Си уже выполняется рантаймом (рантаймом cpp!), который обычно включает оптимизирующий генератор кода.

Преподобные гении Керниган и Ричи применили монады из теорката к разработке языков программирования значительно раньше, чем все остальные. Им пришлось немного прогнуться под антитеоретические штуки наподобие # undef, и правила определения области действия получились не так чисты, как, скажем, в лямбда-исчислении или Scheme (но, подождите, даже Джон Маккарти неправильно определил область действия в Лиспе.)

Следующим функциональным языком такого уровня стал Хаскель, где тип Си был сделан абстрактным ("IO"), хотя его всячески портили сектанты-вероотступники Черч, Карри и Милнер,
пока святой Wadler не допилил его до теоретически почти идеального... но по сути он остался не более чистым функциональным, чем Си + cpp.

Поэтому если хотите функциональности + мощнейшей экосистемы, пишите либо на Си под Линукс, либо на F# под .NET.
И забудьте про Java.

.

Облако драгоценностей за неделю.

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

Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).

Засада с валидацией

Предыдущие серии:
Засада с микросервисами
Засада с исключениями
Засада с инициализацией
Засада с контроллером


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

Мне кажется, что ещё чуть-чуть, и продавцов курсов "за полгода на работу, зп начинающего 70,000 рублей" начнут подкарауливать на улице их клиенты...

Как только вы освоите универсальные основы разработки, создание 99% программных систем действительно станет для вас довольно простым делом. Причина в том, что всё в разработке софта сводится к трем очень специфическим вещам: [...].
...Я говорю это для того, чтобы придать вам уверенности: чтобы добиться успеха в качестве разработчика, вам просто нужно по-настоящему овладеть тремя мета-навыками ↑↑↑

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

СильныеИдеи++
42. SOLID25 : [3...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.

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

=

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

=

Новые материалы для ментатов Лаборатории.

В раздел "Элитный программист" добавлен материал
70) Шиза для программиста - 4.

В СильныеИдеи добавлен материал "120) Нечистый эффект наблюдения чистых функций".
В функциональной архитектуре (даже просто на уровне in small) чистые функции не могут выполнять "нечистые" действия. С другой стороны, наблюдение за результатом чистого вычисления будет побочным эффектом.

=

"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.

Гайд по "Calculus of (Inductive) Constructions",
этим летом 💯 будет готов.
Контент весь я сделал, осталось отформатировать для библиотечного сервера, на неделе закончу.

Главный приятный вывод от погружения в CoC / CIC — что она сильно ограничена узким диапазоном задач (доказательства теорем и корректности программ, верификация свойств, автоматический вывод доказательств...), на что заточены все эти европейские пруверы Coq, Agda, Idris, Lean, которым обучают всю Европу и США — и за пределы CoC они выйти не могут, чтобы стать хотя бы немного ближе к ИТ.

Поэтому как закончу "кубики", берусь за разработку думательных паттернов (мантр) in large в парадигме гомотопической теории (переводим в неё software и system design сколько получится). Ну например простейшее - вместо
"внешний ключ связывает таблицы" мы можем думать об эквивалентности путей между типами данных, выявляя некорректные или избыточные связи ещё на этапе проектирования; составные ключи — это типы h-уровней (формальный способ рассуждать о разных уровнях уникальности данных и их отношениях);
с помощью высшего индуктивного типа Pushout корректно склеиваем разные типы (результат слияния таблиц будет консистентным независимо от порядка операций) и т.д. и т.п.
Ну и сам hott-кодинг конечно (абсолютный на сегодня уровень абстракций).

=

Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 25 уровней из ~50 альфа-версии,
этим летом бета-версия 💯 будет готова.

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

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

Кубики в целом более интуитивная модель для программистов (кубы vs абстрактные пути) + прямая связь с параллельным программированием, Но для меня важнее сила абстракций, а она топчик в гомотопической теории конечно.

CTT:
Явно моделируем переходы и трансформации.
Получаем формальные гарантии корректности через композицию путей.
Можем проанализировать (например с помощью солвера Z3) все комбинации состояний.
Чётко видим и понимаем инварианты на гранях куба.

=

Ну вот совсем примитивная "кубическая" метафора которую вы можете использовать прямо сейчас.

Измерения куба:
- Ось X: Версии схемы данных (0 -> 1)
- Ось Y: Состояния данных (валидное -> невалидное)
- Ось Z: Время (t0 -> t1)

Грани куба (Face):
- (X=0): Старая схема
- (X=1): Новая схема
- (Y=0): Валидные данные
- (Y=1): Временно невалидные
- (Z=0): Начальное время
- (Z=1): Конечное время

Пути (CubicalPath):
- Миграция: путь по X (схема -> схема)
- Валидация: путь по Y (невалидное -> валидное)
- История: путь по Z (время -> время)

Безопасные миграции с сохранением истории.
Отслеживание состояний валидации.
Возможность отката изменений.

Или вот:

Измерения куба:
- Ось X: Узлы распределенной БД (node1 -> node2)
- Ось Y: Уровни согласованности (eventual -> strong)
- Ось Z: Типы данных (simple -> complex)

Грани:
- (X=0,1): Состояния узлов
- (Y=0,1): Гарантии согласованности
- (Z=0,1): Структуры данных

Пути:
- Репликация: путь между узлами
- Усиление согласованности: путь по Y
- Преобразование типов: путь по Z

Управление распределённой согласованностью.
Адаптивные уровни гарантий для разных типов.
Безопасные преобразования между представлениями.

=

Вы это всё прочитали и подумали про себя "мне всё понятно! буду такие же кубики делать!". Это - 💯 признак что вам вообще ничего не понятно. Предлагаю тогда - возьмите жпт и разберите самостоятельно. Вы наверняка умнее меня и сами всё знаете. Хотя я так не думаю.

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

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

...на работе активно пошли собесы и скрининги. Стараюсь сейчас задавать много новых вопросов, чтобы повторять/углублять старый и изучать новый материал. Без этой активности совсем грустно было: теория быстро выветривается, если ее активно не применяешь. А ходить на большое количество собеседований в качестве кандидата съедает много сил и времени + в целом не добиться такой же интенсивности.

...Продолжаю откликаться на вакансии в hh. На этот раз оставлял отклики пачками. Активность hr заметно выросла. Поговорил с hr'ами из трех компаний. Одни предложили ЗП для Senior/Lead в 350 т.р. :)), по второму жду ОС, третьи (аутстаф) сами предложили трудоустройство full-time трудоустройство параллельно с основным местом работы.

...Есть две проблемы:
- understaff
- идиоты в платформе, которые ничего не могут без меня сделать. Хорошо если бы они просто не могли, так они ломают все.
...А сегодня сели чинить, оказалось последний бекап лежит за ноябрь 2024 года.

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

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

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

...Вернулся из оптуска, нифига не отдохнул (семья)

...Задач писать новый код на сотни строк пока совсем нет

...Затем позвали на финал с тимлидом. Не сразу нашли контакт, но в итоге оффер на 500 т.р. после вычета налогов получил. Сначала просил 450 и.р., но сторговаться).... Но у меня на текущем месте больше зп, поэтому сижу ровно :)

=

Я это запостил, потому что вам нравится такое читать.

Но вот что вам не нравится читать: более полугода 2025 уже прошло, а насколько выросла за этот период твоя зарплата? На какие-нибудь жалкие 10%, в разы меньше реальной инфляции? Если выросла вообще.

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

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

Иногда я надеваю наушники во время программирования, но на самом деле ничего не слушаю.

Научный свежачок от Apple: The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity.

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

LRM далеки от AGI: их "мышление" поверхностно и не масштабируется. Они не могут строго следовать даже готовым алгоритмам. Бесполезная трата ресурсов после нахождения решения. Математические бенчмарки уязвимы для оптимизации: нужны наборы, где нельзя угадать паттерн.

Преимущество LRM в математических бенчмарках (AIME, MATH) -- артефакт контаминации данных. Их "рассуждения" -- оптимизация под среднюю сложность, а не обобщаемый навык. За порогом сложности LRM не просто ошибаются -- они отказываются от попыток решать (снижают усилия, хотя контекстное окно позволяет продолжать).

Нужны архитектуры, способные к последовательной верификации и алгоритмической строгости (например, кубическая теория типов).

Интересно, какие показательные тесты авторы подобрали -- пазлы.
Hanoi (экспоненциальная сложность), Checker Jumping (квадратичная), River Crossing/Blocks World (линейная) — покрывают нужный спектр тестов. Но в Tower of Hanoi LRM делают до 100 верных шагов, а в River Crossing ошибаются на 5-м шаге.
Рекомендую кстати поиграть в River Crossing.

Простые задачи: Раннее верное решение -- затем "перемудривание" (генерируют ошибки).
Средние задачи: Верное решение появляется позже после проб и ошибок. LRM тут проявляют преимущество над LLM за счёт "размышлений".
Сложные задачи: Нет верных решений в цепочке рассуждений. Полный коллапс всех моделей (точность -> 0%), несмотря на огромные вычислительные ресурсы.

Программисты, выдыхаем и идём неспешно разбираться в software design.

Менторство -- это игра вдолгую, на многие годы. Эти бедолаги не будут полноценно использовать твой способ, пока их собственные подходы не принесут им достаточно боли. Относится это и к развитию карьеры, и к изучению computer science.

.

Действительно умён тот, кто освятил и свой ум.
прп. Паисий Святогорец

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

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

Глубинное государство Сети -- это компании, которые притворяются, что дарят вам подарки. Не поддавайтесь.

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

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

Мы должны вызывать общественный резонанс, когда какой-либо онлайновый бизнес просит творческого профессионала работать бесплатно, "за лайки", просто выкладывая свою музыку, рисунки, видео. Это позорная практика, и к ней следует относиться как к таковой.

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

Но иногда одарённые люди действительно сопротивляются. Андеграунд жив.

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

Никакой найм в русской айтишке не сломан, в ней всё прекрасно 💥 и развивается именно так, как и должно быть 💯

Программирование рассчитано на умных и грамотных людей, и те, кто "изучает" веб-фреймворки 🤮 , по определению вообще в ИТ не нужен. Чем их меньше, тем здоровее индустрия, AI и так уже всех лишних десятками тысяч заменяет, очень доволен 👍

Если человек не понимает например, почему функциональное программирование алгебраическое, а ООП - ко-алгебраическое, то лучше бы ему вообще никогда работу программистом не найти 👊

Или, довольно популярна тема абстрактных типов данных, которые в ООП часто смешивают с абстрактными классами или публичными интерфейсами, но они лишь внешни обманчиво схожи, а по сути кардинально отличаются. В ООП реализация "приватна для объекта", когда каждый объект представляет собой некий уникальный вариант данных, но вот добавить ему новые операции невозможно. В АТД же ровно наоборот: в нём реализация "приватна для типа", где операции добавляются легко и просто, а вот изменчивость по данным может потребовать изменение определения и самого АТД, и реализации всех операций. Я на треке ООАП немножечко встроил в гайды базу ООП+АТД от Бертрана Мейера, но в целом поразительно, если кто-то не читал классику "On Understanding Data Abstraction, Revisited". И уж не говорю про базу 1978-го года от святого Рейнолдса 🙏 по абстракциям данных "User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction".

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

За каким хреном остальные люди вообще лезут в цифровую отрасль, не понимаю 💩

К сохранению душевного мира нужно чаще входить в себя и спрашивать: "Кто я?" "Где я?"
прп. Серафим Саровский

Невероятно мощный лайфхак, который забустит и вашу карьеру и вашу жизнь. Несмотря на то что он совсем простой, 98% бедолаг не способны следовать даже ему, поэтому вы получите огромное конкурентное преимущество.

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

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

Я таким образом например просто в диалоге deepseek+дипсинк получил супер-рекомендацию по здоровью/постковиду, которая дала эффект в тот же день, и которую мне буквально десятки врачей три года не могли сформулировать -- просто потому что работают по давно отставшим от жизни шаблонам и не заинтересованы в саморазвитии.

Почему пробовать разные модели? Потому что вам нужно точное попадание конкретно в вашу ситуацию.

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

Где я?

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

Другое дело, что их надо уметь правильно готовить.

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

Да в принципе и прогрев норм, если бы всё остальное было читабельно.

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

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

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

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

Разработчики думали, что работают на 20% быстрее с AI, но на самом деле они программировали на 19% медленнее, когда у них был доступ к ЖПТ, чем когда у них его не было.

Вайб-кодинг - это когда 2 разработчика генерируют техдолг, который ранее выдавали 50 программистов.

Пейпер:
Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity

.

Облако драгоценностей за неделю.

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

Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).

Засада с неочевидно полезными сущностями.

Предыдущие серии:
Засада с валидацией
Засада с микросервисами
Засада с исключениями
Засада с инициализацией
Засада с контроллером


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

...Следующая методика повышения личной продуктивности -- [...] -- была разработана группой IT-компаний, включая Oracle и British Airways, объединившихся для создания стандарта быстрой разработки.

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

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

СильныеИдеи++
43-44. SOLID25 : [4,5...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.

=

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


=

Новые материалы для ментатов Лаборатории.

В раздел "Элитный программист" добавлен материал
71) Шиза для программиста - 5.
Как только вы освоитесь c полноценной практикой Шизы, она принесёт вам огромную пользу во многих отношениях: вы не только сможете длительно сохранять концентрацию во время выполнения самых скучных заданий, но и сможете быстро входить в состояние потока, даже если рутинные и повторяющиеся задачи будут вам препятствовать.

=

"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.
Программно полностью смоделировал CTT, учебный контент готов на 70%.

Гайд по "Calculus of (Inductive) Constructions",
этим летом 💯 будет готов.

Но если вы хотите оставаться "нормальным" - эти материалы вам не нужны. Если вы боитесь узнать правду о своих способностях - не изучайте гомотопическую теорию. HoTT/CTT только для тех, кто всегда чувствовал себя белой вороной в программировании.

=

Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 25(+0) уровней из ~50 альфа-версии,
этим летом бета-версия 💯 будет готова.
Добавил ачивки, новые бонусы за помидорки и т.п.
В перспективе встрою в него тайм-трекер с точностью до минуты (а может, и до секунд:). Только тибетские мастера способны :)
Ну потому что если вы не способны даже 15 минут потратить на саморазвитие, вот тогда наглядно поужасаетесь, сколько часов собственной жизни ежедневно вы сливаете впустую.

p.s. в смысле август через две недели??