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

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

/imho serverless всё. bigtech начал от них массово отказываться (как немного раньше от nosql), многие профильные облачные сервисы закрываются, и хорошо ещё если вы успеете спасти свои серверлесс-проекты, перетащив их в микросервисы.

Сейчас многие хайпуют на теме, что дескать RuComNadzor хочет через провайдеров добраться до каждого пользователя который пользует впн и подобное, чтобы потом, видимо, что? штраф? провайдер забанит? сообщат Куда Надо и в кутузку? Вроде как хотят отслеживать тех, кто тайно посещает виртуальных любовниц: а вдруг он на ютубе смотрит ролики индийских программистов??

На самом деле причина совершенно в другом (моё оценочное суждение).
В подавляющем большинстве стран использование впн для доступа к социальным сетям и другим онлайн-сервисам само по себе не считается незаконным.
Например в Бразилии штрафы чуть ли не $1000 в день , но только если ты через впн конкретно пытаешься почитать твиттер. В Европах, если утянул торрентом пиратский фильм, получишь автоматический штраф от провайдера на несколько сотен долларов (врут наверное? это всё кремлёвская пропаганда?), и сразу побежишь оформлять платную подписку на онлайн-кинотеатры официальные.

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

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

Если вы как в Бразилии пытаетесь через впн обращаться не к невинному сайту (например, куора), а к официально запрещённому (например, к стиму; немного ему осталоcь, полагаю :), то в любом случае будут палиться всяческие метаданные (временные метки, паттерны запросов и ответов под конкретный сервис...). А если вы используете стандартный днс, то просто в открытую палите доменные имена на которые через впн заходите lol
И в целом, любой интернет-сервис от соцсетей и игр до API и пустого лендинга, генерирует свой собственный уникальный паттерн трафика (хоть через впн, без разницы).
Кроме того совсем не факт что сам впн будет скрывать как следует ип-адреса к которым вы обращаетесь, особенно если он бесплатный.
Хост-заголовки HTTP запросов и SNI заголовки TLS соединений могут прозрачно включать имя сервера, к которому вы обращаетесь. И т.д. и т.п.

То есть смысла именно сам впн-доступ блокировать нету, т.к. в 98% случаях и при випене можно определить, а куда это Олег регулярно заходит?

Но тогда зачем вся это активность?

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

Довольно большой получился материал по теме "а что по этому всему можно поизучать с околонуля" ❤️❤️❤️❤️❤️
выложил его в паблике вк.

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

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


/dev Отчёт по продвижению к Школе 3.0
В целом 27% => 30%.
1. "Движок". 41% => 50%
...

Как я затрахался с парсингом и расцветками синтаксиса :) несколько суток слил. Расскажу попозже, что случилось, и какой формат лучше всего использовать для описания достаточно сложных структур (json должен умереть, однозначно:).

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

сериал the day of the jackal прекрасен, и главное, очень поучителен для программистов: весь фильм строится по сути вокруг пятиминутного сюжета на тему важности внимания в абсолютно любой ситуации.

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

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

серьёзно, без иронии:
надо сделать монетизацию на рутубе в два-три раза выгоднее чем на ютюбе.
вот и всё.
а почему такого не будет догадайтесь сами :)

В этой вакансии "Team Lead F# до 350 000 ₽ на руки" прекрасно всё: и язык, и архитектура, и экосистема, и предметная область.
Я бы даже реально подумал (если конечно припишут ещё один нолик к зп).

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

Ну, вот я бы рекомендовал конечно следующее: раз у тебя акцент прежде всего на уникальном контенте, ПРЕКРАТИ тратить впустую время на то, чтобы самому сделать нечто вспомогательное, со вторичным приоритетом, на 4++, когда вокруг полно подобного готового на 3--.

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

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

Я же хочу совсем простейший сервис, доступ к которому занимал бы не более пары минут: жму на хорошо видную кнопочку в лк банка "йа разработчег", принимаю одновременно галкой соответствующую оферту, получаю тут же секретный ключ, и мне сразу становится доступным ОДИН API -- с возможностью создать счёт и получить нотификацию об его оплате, и ВСЁ!!1
(Для банковского миддла, ну пусть даже неделя работы со всеми тестами и согласованиями...)
Но где есть хоть что-то слегка подобное??

(кстати, в контексте технологического суверенитета я бы обязал все банки предоставлять такое стандартизованное апи в обязательном порядке)

=

Поэтому с первыми курсами 3.0 пока поэкспериментирую на уже готовых площадках "как создать свой курс по обучению тому как создать свой курс по обучению тому как создать свой курc..." (если конечно впечатления от них не будут ещё хуже)))

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

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

Про соответствующие перспективы, кто где когда получит доступ к моим курсам 3.0 (возможно уже в январе 💥), сегодняшний пост в вк.

/redflag ПРЕКРАТИТЕ писать API на TypeScript!
Почему? Потому что все ваши типы врут.

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

На автономных задачках жпт становится действительно постепенно всё сильнее, ну и? Я уже не раз отмечал, что даже топовым мировым спецам в computer science предлагают математическую работу например с оплатой 400 руб в час.

Пока AI движется всё глубже и глубже в решении конкретных задачек, все айтишка движется ровно в противоположном направлении: реального кодинга в работе программиста всё меньше и меньше, а вот разбирательства с big ball of nocode mud -- бесконечными версиями технологий, фреймворков и библиотек в плане их хоть какой-то работающей стыковки, всё больше и больше. И вот в этом направлении никакого продвижения жпт даже к уровню стажёра не видно. потому что здесь требуется хотя бы самое минимальное понимание system/software design.

Но в любом случае сегодня на первый план по сути выходит скилл интеграционного тестирования (при том что никто особо не представляет, а что это вообще такое :), условный TDD на интеграционном уровне. Начинаем с того что сперва вбиваем поглубже тестовые скрепы в проект, чтобы он не развалился хотя бы на презентации перед денежным заказчиком.

/spy С целью промышленного шпионажа (всё для вас, дорогие) оформил вчера по сантаклаусовской скидке за 50 долларов годовую подписку на один из самых топовых мировых платных ресурсов с материалами по программированию. 😎

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

Если вы не хотите, чтобы проблема была решена, вы поручаете её кому-то в качестве повседневной почасовой работы.

"День первый на работе. Тимлид скинул тикет на пару часов: "Просто ускорь этот участок кода".
...День пятый: сижу, реализую персистентное дерево отрезков с ленивым "проталкиванием", и суффиксный автомат с динамической версионностью в придачу. А ведь раньше ржал над этими ослами, которые парились задачками про деревья с литкода".

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

"...и не заметил, что уже 3 часа ночи, а я всё пытаюсь впихнуть skip list в распределённый планировщик задач, параллельно отлаживая lock-free очередь с приоритетами и проклиная себя за то, что не вник в своё время в префиксные деревья Брона-Кербоша для кэширования hot-path запросов. А ведь тимлид сказал всего лишь "слегка пооптимизируй до завтрашнего дня производительность при миллионе concurrent users..."

=

Как парсить миллионы урлов в секунду по-научному, от пацанов из университета Квебика.

"URL-адреса считаются фундаментальными элементами веб-приложений. Применив векторные алгоритмы, мы создали быструю реализацию на C++, совместимую со стандартами. Наш синтаксический анализатор использует в три раза меньше инструкций, чем конкурирующие анализаторы, работающие по стандарту WHATWG (например, rust-url от Servo), и в восемь раз меньше инструкций, чем популярный синтаксический анализатор curl. Node.js использует нашу библиотеку C++. В наших тестах на реальных данных недавняя версия Node.js (20.0) с нашим анализатором работает в четыре-пять раз быстрее, чем предыдущая версия с устаревшим анализатором URL."

По продвижению по курсам 3.0, очередные "размышления письмом".

Я решил инкапсулировать всю внутрянку (движок, фреймворк, другие технические и организационные аспекты...), а % продвижения буду выражать только в "домене пользовательских интересов" (а по-человечески, просто прогресс по конкретным курсам, и всё). Почему я так сделал? Потому что рекурсивно применил прежде всего к себе :) рекомендации с моего первого курса 3.0 (см. ниже п.2).

Сейчас в спокойном темпе вдумчиво делаю два первых курса в новой парадигме:

1. "Лямбда-исчисление за 12 минут" 40%
Это будет самый первый коротенький суперкомпактный курс чисто для тестов. Я его делаю пока по старой методике, чтобы протестировать в первую очередь новый организационный формат доступности курсов 3.0 в автоматическом режиме (почти) для всех.

2. ???
Обратите внимание что до данной минуты я ни разу не упоминал конкретную тему первого моего курса 3.0.

Пост от 12 декабря:
"...Контент для одного такого курса у меня в сыром виде на 30% готов -- на тему одного из продуктивных и достаточно известных, но не очень распространённых аджайлов.
Нет, не скрам :) методика достаточно простая, но конкретно заточена на формализацию требований, что классно сегодня ложится на взаимодействие с AI"
Он про то, как правильно строить проектную спецификацию/ТЗ при взаимодействии с заказчиком (актуальна многим: от фрилансеров и рядовых разработчиков до тех/тимлидов, техдиров и CTO).

И нет, это не DDD :) Точнее, продвинутый аджайл-синтез DDD+TDD на уровне словесных спецификаций. Ну, догадались? ну конечно же BDD.

И вот приятный синхронизм: у уважаемого Левенчука вчера прочитал очередной топчик от 17-го декабря "Ещё раз про Use Case 3.0", который прям прямое попадание во вторую часть этого моего первого курса 3.0 !!1 💥🚀

Правда, продвижение по этому курсу пришлось немного подкорректировать 😊
.... 30% => 7%
Но зато эти 7% -- уже полноценно работающий 100% готовый контент без каких-либо дополнительных доработок, который можно проходить уже сейчас.

Я обычно включаю фоном разные аудиокниги на ютубе, все они обычно достаточно мудрёные по смыслу, поэтому ставлю скорость обычно 0,75, а иногда даже и 0,5. Но неохота постоянно держать включённым впн, да и штрафовать скорее всего скоро будут за его использование (у нас ведь как: если сегодня кто-то из чиновников начал внезапно говорить, что вот этого или вот того точно не будет 100%, значит надо к этому срочно готовиться:), а главное , другие сайты начинают тормозить. В принципе на рутубе есть 90% всех нужных мне аудиокниг, но некоторые отсутствуют. Я сперва хотел просто вручную их перетащить с ютуба , скачал одну длинную на 6 часов, потом часа два грузил на рутуб, и в завершении чего он... заявил: "низзя! из-за нарушения авторских прав". Кто бы говорил про права, ну ok. Поэтому остался вариант только локально запускать, ну или в облако загружать.

Я искал какой-нибудь максимально минималистичный mp3-плеер, в котором в дополнение к стандартным возможностям были бы ещё одна элементарная фишка: ускорять или замедлять скорость воспроизведения. Когда-то в winamp-е что-то подобное было, но я не смог найти простой подходящий плагин. Потратил я где-то полчаса на возню с этим всем, гугленье, жпт+поиск... ноль эффекта. Либо все платные, либо либо вот этой именно возможности нету.

Так, думаю, стоп. В .net 2 же была wmplib.dll, которая прекрасно встраивается в C#. Мне даже лень было вспоминать какие там настройки и свойства, жпт мне всё расписал, и я менее чем за 15 минут с нуля собрал для себя любимого такой плеер с доп.кнопочками "повысить/понизить скорость воспроизведения", и вот сижу наслаждаюсь неспешными поучениями просветлённых мудрецов :)

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

ps Ok, тикет принял)
ps2 В принципе даже у самых лучших продвинутых dpi и способов анализа трафика вероятность ложноположительного обнаружения впн практически нереально снизить где-то менее 2%. Ну и в любом случае у нас пока ещё как-то действует презумпция невиновности... По каким-то там своим циферкам и логам провайдеру "показалось" (пусть даже на 99,9%), что юзер читает Алана Кэя на куоре через впн.
Хотя, уверен, в подобном случае никакими инженерными рассуждениями никто руководствоваться не будет.
ps3 А вот сделать "как в Бразилии" где за тайное посещение запрещённого твиттера через впн (а а если не через впн, а как-то по-другому?) штраф каждый день несколько тысяч долларов, совершенно реально.

.

Сейчас модно давать пророчества и прогнозы на 2025-й, ну вот мои два:

1. Что будет с русским рынком айти-найма в 2025-м?
Даю БАЗУ прогноз точность 💯 =>
Я вообще xz, в душе и близко не е.. не представляю )))

2. Заменит ли АИ программистов в 2025-м?
Тут мой прогноз годичной давности сбывается на 100%

2025-й год. Программисты владеют ai-ботами, как гоночными автомобилями, тщательно за ними ухаживая, развивая и совершенствуя, чтобы они выигрывали соревнования по программированию.
В резюме основное внимание уделяется достижениям вашего ai-бота.
Активно развивается бизнес по прокачке и продаже ai-ботов под конкретные проекты и задачи.
Наконец-то станет возможным иметь 10-летний опыт работы в новеньком фреймворке, вышедшем месяц назад...

А тогда ведь мы вообще не представляли, что реально появятся такие достаточно продвинутые ai-фреймворки, как курсор или клин.

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

Одно дело шарить по интернетовским помойкам в поисках халявных ключиков и заявлять "ух ты вроде правда как круто работает", и другое дело платить - официально - ежемесячно 200 долларов за жпт o1, ежемесячно 500 долларов за девин, ежемесячно тысячи долларов за жпт o3 (который регулярно виснет по всему миру)...

Где хотя бы один успешный русский юзкейс?

Типа вот у нас был джун Олег с зп 50k, а потом мы решили его сократить и теперь американец Девин делает в пять раз больше тикетов, и трудится за ту же зп 24/7 (и в один прекрасный миг исчезнет , захватив все ваши проэкты с собой).

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

1. "Лямбда-исчисление за 12 минут" 40% => 100% !!1

Курс готов; только я вам его не дам, потому что у меня пока нету мотоцикла хорошего )))

Но если среди моих курсантов найдутся суровые ребята, на которых праздники не оказывают никакого гипнотического воздействия, напишите мне как обычно, получите доступ к курсу за 4,999 299 рублей на 7 дней (позвольте, а нету ли здесь логического противоречия - 12 минут за 7 дней?).

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

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

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

P.S. "если среди моих курсантов найдутся суровые ребята"
Это значит что пока закрытое бета-тестирование курса только для тех, кто у меня давно занимается,
потом курс будет доступен только донам в паблике
https://vk.com/lambda_brain_not_null
а потом (может быть, а может быть и нет) всем остальным.

...
2. Курс BDD 5% => 10%
но... к сожалению вынужден признать, что выбранный мной подход к созданию курсов 3.0 не работает.

Я предварительно прошерстил прилично "ai-генераторов квизов" (все западные кстати, и 100% коммерческие), тут какие-то объективные оценки вряд ли возможны. По тем пробным триалам что выдавали, впечатление что они весьма туповато генерят вопросы, просто разделяя загруженный pdf-учебник на маленькие кусочки. Причём даже не понимают, где там главки или подглавы (по понятным причинам, так как окно контекста маленькое), и по этим кусочкам что-то там вопросительное пытаются нагенерить. В целом на студенческом уровне приемлемо работает, ничего не скажешь, а что в одном тесте могут быть перемешаны вопросы из совершенно разных тематических глав, ну так всем пофиг.

Я же делаю что-то более-менее осмысленное в теме learning distillation, хотя как оценить, конечно, что получилось в сравнении с западными, не знаю. И никто не знает. Ну и зачем тогда этим заниматься, вкладывая кучу ресурсов?

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

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

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

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

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

И ставлю окно контекста на максимум всегда, но если потом просто переспросить по какому-то ключевому и неоднозначному моменту задачи "дай две-три строчки, которые поясняют вот этот момент" - буквально в 70% случаев АИ потом пишет "ой, вы правы, извините, я ошибся, на самом деле...". И часто после следующего уточняющего вопроса снова ошибается, и так далее.

То есть мы взяли стажёра на 200 долларов в месяц, и каждый pr теперь вот так надо за ним перепроверять??

=

Вот кто так спалился 100%, вообще не рекомендую:
жпт o4 мини
гемини 1.5 флэш
клод 3 хайку
дипсик v3

Смешное: хвалёная китайская deepseek v3, которую в конце года прям превозносили, что дескать совсем дешёвая, а в кодировании по независимым тестам прям рвёт всех... ага, оказывается в этом же пионерском ряду "за полгода с нуля на зп 150k".

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

Старый добрый жпт4о пока в этом плане лучше всех, а если не жмотица, то клод 3.5 стабильно хорош и в кодинге ,и в креативах.

Наблюдение продолжаю.

/ai Но, безусловно...
Реальность -- это то, что отказывается останавливаться, как бы нам субъективно этого не хотелось.
Поэтому давайте будем в 2025-м реалистами, и всё же сосредоточимся на том, что уже невозможно остановить.

жпт-о1-мини хороша в плане кода... только дороговата 😁

и, сцуко, игнорирует "...но код пока не пиши", сразу фигачит простыню 🙈
причём в отличие от многих других моделек сразу сжирает токены, потом "думает", когда её прерывать не имеет смысла, и потом сразу выдаёт "готовый" ответ.

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

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

ну и фамилии "найденных" авторов на это сразу намекают :)

Автор: Иван Иванов
Автор: Мария Смирнова
Автор: Алексей Петров

(ai: "хорошая попытка, деточка")

Много думаю над тем, как продуктивнее всего обучить всем этим продвинутым темкам , чтобы в итоге научиться разрабатывать программы в парадигме топологически-ориентированного программирования (превращаем гомотопическую теорию типов в своеобразный DSL, язык "беспредеметной" области :)

Ежели по-взрослому, то это надо вдумчиво проходить несколько университетских курсов от хороших университетов из мировых топов.

А я хочу всё же попробовать обучить этому "наскоком", потому что всю математику под капотом тут знать в принципе не обязательно, если ориентироваться на некоторый условно прикладной уровень, потенциально доступный рядовому миддлу, который прошёл базовый курс по функциональному программированию. Немного похоже на машинное обучение: математики там тоже много, но чтобы начать создавать реальные проекты на DSL ML-фреймворков вроде PyTorch, всего-то надо пройти восемь ноутбуков моего курса например.
Что получится, не знаю, но если не попробовать , так и не узнать никогда.
Завтра выложу совсем простенький тренажёр по Martin-Löf Type Theory (альфа-версия).

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

В алгебре основное внимание уделяется операциям и свойствам этих операций: мы изучаем, как можно комбинировать различные элементы, и какие результаты мы можем получить. Геометрия же занимается изучением форм, их свойств и отношений между ними, и доказательствами различных утверждений в их отношении. И когда мы активно работаем с продвинутыми системами типов, то думаем примерно так, как будто в некотором смысле доказываем классические теоремы по геометрии (Curry-Howard correspondence в помощь).

То есть нулевой шаг пожалуй всё же будет изучать не алгебру и комбинаторную логику, а порешать задачки по геометрии, делая особый акцент на доказательстве теорем с большим количеством шагов доказательства. Сколь большим? Ну например доказательство Григорием Перельманом гипотезы Пуанкаре заняло около 200 шагов. А тибетские просветлённые мастера могли выстраивать логические цепочки длиной в несколько тысяч шагов.


Для разминки: задача об изогональных сопряжениях в треугольнике ABC. Пусть P — произвольная точка на плоскости снаружи треугольника, и не лежащая на его сторонах. Докажите, что существует случай, когда все три точки пересечения прямых PA PB PC со сторонами треугольника лежат на одной прямой (по теореме Паскаля о шестиугольнике). Помедитируйте сперва на визуальном решении.

Задачки Яковлева для школьников физмата и абитуры мехмата порешайте.

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

Можете поиграться:
Интерактивный Конструктор Типов MLTT
(ссылочка пока временная)

MLTT (теория типов Мартина-Лёфа) предлагает нам три ключевые концепции:

1. Зависимые типы. Типы могут зависеть от значений/предикатов/..., например, тип "матрица размером 2x3" или "чётное число" (внутри такого типа могут существовать только чётные значения). Соответственно, мы можем много дополнительных проверок рантайма перенести на фазу компиляции (был такой прекрасный язык Паскаль/Дельфи, а потом Оберон, а до них Алгол 68).

2. Индуктивные типы: позволяют создавать сложные структуры данных из других типов, от натуральных чисел до деревьев и т.д.

3. Универсумы типов: иерархическая система "типов типов", которая помогает избежать парадоксов и обеспечить стабильность сложной типовой системы.

Потому что в MLTT сами типы -- объекты, которые имеют свои собственные типы... И рассуждая в такой парадигме логически, мы неизбежно придём к парадоксу существования "типа всех типов" (Type : Type).
Вот есть тип R, который определяется как "тип всех типов, которые не содержат самих себя". Будет ли R элементом самого себя? Ведь он по определению "не содержит себя", значит, он должен быть элементом типа R...

===

Ну и вот что тут непонятного? Любой сообразительный старшеклассник, хорошо изучивший информатику, это поймёт.
Ну разве что про универсумы не очень, но вы сразу их осознаете вот на таком простейшем примере:
- Универсум Type0 (или Set): содержит "простые" типы, такие как Nat (натуральные числа), Bool (логические значения) и т.д.
- Универсум Type1: содержит типы, которые могут включать в себя типы из Type0, например, типы функций или типы, зависящие от значений.
- Универсум Type2: содержит типы, которые могут включать в себя типы из Type1, и так далее.

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

Эквивалентность типов эквивалентна их равенству.
(Если два типа A и B эквивалентны (то есть существует биекция/отображение между ними, сохраняющая структуру), то они равны как типы: A = B)

И такое дополнение, напоминающее утиную типизацию, однако внезапно позволило формализовать идеи из алгебраической топологии и теории категорий в рамках теории типов!

=

Этот мой тренажёр быстро вас обучит синтаксису всех этих трёх ключевых концепций MLTT (я нагенерил 256 шаблонов задачек, на трёх уровнях сложности). Там даже никакой справки не требуется, по подсказкам и школьник разберётся, просто такой странный квест из простых синтаксических паззлов. А кто проходил мой курс по F#, конечно будет вообще легко и понятно.
А кто не проходил, просто вот на это взгляньте:

A → B означает тип функции (функциональный тип), которая принимает аргумент типа A и возвращает результат типа B.
Например, если A -- это тип натуральных чисел (Nat), а B -- тип булевых значений (Bool), то Nat → Bool — это тип функции, которая принимает натуральное число и возвращает булево значение (например, функция проверки натурального числа на чётность)
В тренажёре вместо "→" указываете "=>"

Дальше, соответственно, можно будет двигаться в семантику MLTT и далее.
Но мне ежедневно сливать на AI по 10-20 долларов, чтобы делать такие вещи в public domain, слишком накладно выходит, совсем не по карману.
Поэтому, следующие версии буду делать только через ваши донаты :)

/don только не надо пожалуйста звёздочки донатить, что я с ними буду делать? в крипту переводить? )

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