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

Во-вторых, если серьёзно, на самом деле вы программируете на чистом функциональном языке препроцессора 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. в смысле август через две недели??

Если вы можете инвертировать двоичное дерево, вы можете делать в программировании всё, что угодно.

Нередко спрашивают, и я в принципе раньше уже отвечал, но эта темка будет вечной (и это прекрасно).

Я Вас регулярно читаю и задумался о том, что хорошо бы мне подтянуть математику. (В последний раз вышмат был в универе лет 7-8 назад).

Хочу узнать у Вас куда можно записаться, что посмотреть и порешать. В целом хочу понять что из матана может потребоваться для того, чтобы заниматься дальше комфортно заниматься на курсах и стать полноценным Ментатом. (Думаю пока со Смаллиана начну.)

1. Матан не нужен 💯
Собственно, в закрепе Лаборатории вконтактнике уже много лет пост висит, какая математика/computer science нужна Программисту.

2. Смаллиана однозначно рекомендую просто в вакууме, ни с чем не связано, "Передразнить пересмешника" в первую очередь. А с детишками полезно вместе поразбирать его легендарные "Принцесса или тигр", про Алису серию, и т.д.

3. В матрице компетенций (в личном кабинете), там 50+ треков развития, и среди них есть трек по математике вот буквально с самого начала, с околонуля.

4. Если кто-то прямо очень-очень серьёзно настроен в математику, я помогаю индивидуально даю рекомендации что поизучать, и самое главное, в каком порядке -- до топового уровня HoTT именно на уровне профессионального математика. Но за всё время было всего два человека кто пытался, и запала ожидаемо хватило ненадолго, на теории групп все слились. Даже до базового уровня учебника Александрова "Введение в теорию групп" не добрались.

5. Я фактически закончил трек HoTT/CoC/CTT для уровня обычного программиста (надеюсь). Кто проходит три базовых трека второй части Лаборатории -- ООАП, Ясное проектирование и Функциональное программирование (дорабатываю сейчас, кстати), потом по желанию может сразу его пройти.

6. В качестве вводного подготовительного уровня к HoTT, в принципе много раз уже рекомендовал "Типы в языках программирования" Пирса и/или "Программирование: теория типов" (Швецкий, Кудрявцева).

Конечно стоит и SICP прочитать (база, как и TaPL), ну и до кучи "How to Design Programs" (HtDP). Эти три-четыре книги - абсолютный начальный must have для всех, кто хочет изучать computer science.

И затем всю линейку "The Little ...":
The Little Schemer, The Little Typer, The Little Prover...

"A Little Java" кстати вообще всем рекомендую: мозгоразрывающее применение паттерна Visitor.

7. Но если честно, то по хардкору я бы рекомендовал так =>

- прыгаешь сперва с головой в OnLisp

- потом в "Introduction to the MIPS Architecture and Assembly Language"
вроде такого

- пишешь для MIPS/Байкала свой компилятор Лиспа в continuation-passing style

- попутно шлифуешь алгосики по MIT-овскому "6.851: Advanced Data Structures"

Скрипач Кнут Вирт etc вообще не нужен, вместо них "Hacker"s Delight".

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

Колебаний не было.

- Я буду продолжать тренировки! - сказал Пол, и подумал: "возможно, быть ментатом на самом деле ужасно".