Лаборатория Математики и Программирования Сергея Бобровского

...В мировой микро-тусовке по hott-"программированию" (считанные десятки человек) пишут что-то подобное в основном на хаскеле, ну а я сделал на питончике 🙈

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

a) не просто такое реализуешь, а сделаешь "свой солвер" никому нафиг не нужный , и

б) обязательно добавить кубик (это вообще чисто понтовый топчик).
(пять лет назад я пояснял что это: "Кубическая теория типов для малышей") - только тогда будешь считаться cs-просветлённым 🙏

Впрочем, до этой тусовки мне нет абсолютно никакого дела. Буду продолжать эти темки исключительно на русском, и только в рунете (жаль сайт hott ру занят какой-то попсой :).
Хотя кубик будет обязательно.

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

Хотя нет... В хотт 5+ уровень - это уже наверное на премию Филдса 😇
формализация (∞,1)-топосов, моделирование высших группоидов, бесконечно-категорные структуры...

А в генше вроде до сотого левела можно...

С другой стороны, каждый универсум легко бьётся минимум на десяток подуровней для изучения, и для первых двух-трёх универсумов темп прохождения изучения получается примерно как в GI 💎

(продолжение следует)

Сам не ожидал, но я всё же завершил свою специальную научную операцию ровно в День Науки! 💥💥💥🚀💪🏻

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

Где-то в 23:50 я успешно прогнал два заключительных базовых теста (унивалентности и "интеграционные":), и только сегодня утром осознал, что намедни уложился таки в святой день! 🤘🙏☺️

Я реализовал БАЗУ HoTT:

1. Базовые типы и зависимые типы
- Реализация Unit, Empty, Sum, Product
- Система Pi- и Sigma-типов
- Механизм зависимых функций

2. Пути и тождества (Path)
- Реализация путей как равенства
- Операции над путями (симметрия, транзитивность)
- Система доказательств для путей

3. Высшие индуктивные типы (HITs)
- Реализация Circle и Torus
- Механизм рекурсии для HITs

4. Унивалентность
- Система эквивалентностей типов
- Транспорт вдоль путей
- Преобразование путей в эквивалентности

5. Бесконечно-группоидная структура
- Реализация путей высших размерностей
- Операции композиции путей
- Механизм когерентности

6. Усечения типов
- Система n-усечений
- Пропозициональное усечение
- Усечение до множества

7. Иерархия универсумов
- Система уровней
- Кумулятивность универсумов
- Полиморфизм по уровням

8. Гомотопические группы
- Вычисление гомотопических групп
- Пространства петель
...

💝💝💝

(продолжение следует)

...Ну и наконец приближаемся ко дну и пробиваем его 😁

Последний минимальный приемлемый язык -- C#.
Теперь у нас уже нету паттерн матчинга "из коробки" и алгебраических типов данных, существенно проигрываем F# как математической нотации, но зато в девятке появились record types, source generators, а так же продвинутые дженерики:
bool IsConnected<U>(HomotopyType<U, IPath<U>> other) where U : IComparable<U>
и даже метапрограммирование:
bool IsHomotopic<T>(this T value, Func<T, bool> predicate)

3. C# хз, ну если только с F# по каким-то совсем конкретным нюансам не получится. В коре на F# эндпоинты вообще в пару строк задаются 😊

[<ApiController>]
[<Route("api/[controller]")>]
type ProofController() =
[<HttpPost>]
member _.ProcessProof([<FromBody>] req: ProofRequest) =
let response = {
Status = true
Result = sprintf "Processed: %s" req.Theorem
}

...
let app = WebApplication.Create()
app.MapGet("/dwarf", fun () -> dwarf)
app.MapPost("/dwarf", fun (dwarf: Dwarf) ->
... Results.Created("/dwarf", dwarf))
app.Run()

=

Посадка на дно начинается с "хотт на питончике" )))
Задаём термы (лямды, универсы, pi-) как датаклассы, а динамическая типизация позволяет вытворять разные штуки на уровне F#.

По большому счёту конечно всё это можно сделать интерпретацией чисто на символьном уровне, как я пытался на пыхе, но слишком уж велика трудоёмкость. В принципе, 50% MLTT (лямбда-исчисление, аппликация и зависимые типы) я упаковал где-то в 200 строк PHP-кода 👊
Но дальше, когда полезли в индуктивные типы, универсумы и особенно рекурсивные определения, без какой-то минимально адекватной типизации, с тайп инференсом в чисто символьных вычислениях начинается полный хардкор 🤘

4. MLTT++ на Python по-взрослому (термы/значения как типы данных).

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


5. Ну и в заключение пробиваем дно: пыхапы :)
Ничего не могу сказать, с него я начинал - им же и закончу?
Если получится что-то на питоне, то можно в принципе его код достаточно легко конвертнуть в php...

=

HoTT в Lean 4: 3/10 (почти готовая реализация)
HoTT в F#: 8/10 (практически с нуля, но система типов близка к математической нотации)
HoTT в C#: 9/10
HoTT в Python: 10/10
HoTT в PHP: 12/10

=

В общем, буду пробывать в таком порядке:

4. MLTT++ на Python по-взрослому
1. Lean 4 : REST + HoTT
2. F#
3. C#
4. PHP

Успех предрешён и неминуем.

...В принципе можно конечно сделать вообще на Лине 4, самое смешное, что поддержка хотт была в третьей версии, но потом её оттуда выпилили, потому что поддержка унивалентности в ядре Lean оказалась пацанам не под силу 😬 Надо переопределять базовые понятия равенства, конфликты с классическими представлениями о тождестве, нарушается UIP и AC, бесконечные иерархии преобразований, запутанные проверки эквивалентности...

Вроде бы тривиально?

def idEquiv {A : Type} : A ≃ A

Да но мы-то хотим такое с унивалентностью в ядре доказательств 🫢
Классическая теория, что с лицом?

Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции.

Поэтому с одного края: то что я делал на PHP, просто закодировать непосредственно на лине как языке программирования (без каких-то плагинов для ядра), это вообще легко и просто. Но тут засада, что я ведь хочу сделать многопользовательский (веб)клиент. Хотя в лине имеется нативная поддержка concurrency, асинки...

1.1. Посмотреть, можно ли на коленке склепать рестик на лине 4.
1.2. Запилить некую минималистичную поддержку хотт.

=

Другой вариант: использовать F* -- микрософт его прям энергично развивает вовсю. И вроде бы это .NET -- но нет )
Сетевой поддержки у него нету, придётся делать обвязки на ocaml, да и сам он позиционируется прежде всего в направлении верификации кода, Lean конечно посильнее в математическом плане.

Поэтому от F* отказываемся, и следующий шаг -- это наш любимый F#. Вот тут в техническом плане сразу всё становится элементарно, но зато мы резко проседаем по системе типов (прежде всего теряем завтипчики) и уже прилично скатываемся на другой конец, ближе к пыхапы 🙈

Навскидку:
HoTT в F#: 7/10 (практически с нуля)
HoTT в Lean 4: 3/10 (почти готовая реализация)

2.1. Если по п.1.1 возникнут явные трудности, когда немного поэкспериментировать с F#.

(размышления продолжаю...)

Планировал завершить мою специальную научную операцию (гомотопическая теория типов на PHP :) ко Дню Науки...

Кстати с праздником, дорогие! 🚀
(не, я поспешил, он же завтра — в один день с Лыжнёй России :)

Вы же знаете, что финансирование всей фундаментальной математики в СССР было существенно меньше стоимости одного танка? (а как сейчас, вообще военная тайна, я её знаю, но вам не скажу :)

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

Но с другой стороны, искусство и наука требуют жертв, и никакой окупаемости не может быть в принципе...

Король был удивлен: этому человеку казалось, по крайней мере, сто двадцать лет. Неужели он сумасшедший, или... Он не мог ожидать, чтобы эти деревья начали цвести, тем более давать плоды - зачем же ему все это было нужно? Он трудился в старости так напряженно, целый день на жаре. Это была пустынная земля.
Старик засмеялся и ответил: «Нет, я не смогу видеть цветы на этих растениях. Но видишь ли ты прямо за моей хижиной эти огромные деревья, которым тысячи лет? Это те же самые деревья. Они дают мне плоды, дают мне цветы».
Король сказал: «Я могу видеть их, но не могу понять. При чем здесь эти деревья?»
Старик ответил: «Если бы мои предки не посадили их, если бы они также думали, что не смогут видеть плодов своего труда, цветов и плодов деревьев, этих деревьев бы не было. Я не думаю о себе. Я думаю о своих предках и потомках. Я должен оставить им какое-то наследство!»

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

(продолжаю размышления письмом .... сегодня для этого святой день)

кстати, мем в плане темок-топчиков верен на 100% )

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

Пара полезняшек:

-- Nue (standards first web framework) : HTML, CSS, and JavaScript taken to their absolute peak.

-- fish is a smart and user-friendly command line shell for Linux, macOS, and the rest of the family. Finally, a command line shell for the 90s.

Цена дипсика в 5,6 млн.долл. -- это хайп и фейк. Оказалось, что это "всего лишь стоимость GPU для предварительной подготовки", а фактическая общая стоимость исчисляется миллиардами, как и ожидалось.
Подробный срыв покровов тут.

...А может и правда, что к созданию современного AI имеют прямое отношение наработки советских математиков? см картинку.
Invented principles of meta-learning (1987), GANs (1990), Transformers (1991), very deep learning (1991), etc.

Хорошая подборочка: идеи AI-стартапов, на которые YC готов давать денежки (много) в этом году. Интересно про "вертикальные AI-агенты" -- по сути обёртки вокруг жпт, которые однако будут тщательно настроены для автоматизации какой-то реальной, важной работы.
"Трудно заставить такие системы работать правильно, но как только вы это сделаете, рост может быть феноменальным."
Обещают чуть ли не 100 грустных уточек новых единорогов в этой нише.

Я отдельно повёлся на "Будущее разработки программного обеспечения": сырого контента у меня на эту темку полно, ну думаю, "сейчас наконец буду делать курс".

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

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

Вдогонку к опросу: один из более чем дюжины приёмов сражения с dependency hell (в СИ курсантам скоро поясню их все) -- это семантическое версионирование для управления версиями пакетов и определения совместимости между зависимыми компонентами.

Кстати, свежий тренд — обозначать версии как "год + номер", например 25.0, 25.1, 25.2... Его назвали миксом стандартного семвера и убунта-стайл.

Простой лайфхак, как вам гарантированно проходить любой собес:

Вас как специалиста не должно смущать вообще ничто и никак.

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


/dev в вк выложил пост, как объективно и автоматизированно, и при этом легко и просто оценить, насколько качественно спроектирована ваша система.
...Когда вы создали первые 5 классов, спроектировали первые 5 таблиц в базе, вроде всё норм. Но когда вам надо 256-й класс "впендюрить" в забетонированную систему с высокой связанностью (coupling), начинаются сплошные боль и страдание.
А если вы вдобавок используете протекающие абстракции (например, применяя классические паттерны проектирования "интуитивно", "на глазок"... или не применяя их совсем, и выдумывая собственные костыли и приляпки), то они просто убивают смысл всех ваших интерфейсов в проекте.

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

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

Что делать нам с вами? Двигаться в инди-хакерство 💯
Переходите на удалёнку, прокачивайте скиллы software design чтобы делать рабочие задачки на день во много раз быстрее, а высвободившееся время вкладывать в инди- , и делайте ставку в плане денег только на самих себя. Не *****. Верьте в себя!

Я подправил карьерные цели для курсантов в этом контексте, и на бусти для всех папищеков скоро выложу БАЗУ, с чего начать, какой сделать первый шажок в ситуации, когда вы абсолютно не представляете, куда и как.

Вдогонку к опросу "Механическое добавление суффикса Impl к названию класса, реализующего интерфейс в Java" — что интересно, получилось 50/50.

Это считается (считалось:) фактически стандартным соглашением об именовании, и многими IDE поддерживается дефолтно. Да, но...

Тут конечно Java хорошо бы брать пример со своего старшего и более умного брата C#, где не принято использовать суффикс Impl. Вместо этого интерфейсы именуются с префиксом I (IUserService), но реализации получают понятные имена без I, но с уточнением деталей (например, DatabaseUserService). А если реализация подразумевается не одна, то добавляют префиксы, описывающие конкретное назначение или технологию: DatabaseUserService (PostgressUserService, MongoUserService), CachedUserService, AsyncUserService...

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

Осенью 2024-го сразу три курсанта в один день (!) упомянули всуе DI, а потом вскоре и в отзывах пришло на эту тему:

"Тестирование FE - пока есть ощущение, что код я пишу без DI и прочих подходов, которые облегчат интеграционное тестирование с подкинутыми фейковыми зависямостями. С другой стороны я слабо понимаю, а как тестируется визуальное представление веб-компонента :)"

"Начала выстраиваться наконец-то модель ООП,которая изначально выстроена,к сожалению,с помощью Dependency Injection - как и везде сейчас,и слабого курса в универе,где мы просто С++ учили."

"Оказывается, я открыл F-ограниченный полиморфизм в тот момент, когда мне понадобилось, чтобы методы класса-родителя явно (на уровне статического анализа) возвращали и принимали аргументы конкретных типов, являющихся производными класса-потомка. Даже получилось реализовать это в Python, в котором изначально типы не считались такими уж важными. Это инверсия зависимостей на математических стероидах. "

"Я только вот 1 не понял,в конце вы написали про DI в современных приложениях,и это правда очень искажает понимание ООП,но вы написали,что оно увеличивает coupling из-за того,что мы открываем все наши зависимости. А концепт ADT,где мы описываем типы данных только операциями как раз является решением,потому что вся реализация полностью скрыта и лежит на классе реализующим ADT. Но разве с этими DI контейнерами не так? Определили интерфейс,реализовали его классом в который уже внедряются зависимости,и класс как раз скрывает всю реализацию."

Подробно разбираю эту тему в свежем материале для курсантов: 108-й СИ "Не путаем DI и ADT", даю в частности 10 случаев, когда лучше избегать Dependency Injection в рамках ADT, + 10 ключевых причин, почему это качественно разные вещи, и соответственно как это всё правильно готовить.

Чем опасно самообучение 2025? Тем, что 98% материалов мэйнстрима сегодня стремительно устаревает за считанные месяцы, особенно если они делались с прицелом "побыстрее на работу".

Даже с классикой так: вот "Кабанчик" в последней версии пополнился новыми главками.

-- облачные архитектуры и serverless-вычисления с прицелом на облачную AI-инфраструктуру (AWS SageMaker, Azure ML);
-- гибридные транзакционно-аналитические системы (HTAP), для обучения моделей на свежих данных без остановки продакшена;
-- принципы оптимизации хранилищ (S3, Glacier), дабы снижать затраты на хранение больших датасетов для AI;
-- кодирование данных, форматы вроде Avro и Parquet, оптимизация хранения неструктурированных данных для NLP/CV-моделей;
-- метаданные и управления схемами, важность версионирования данных для интеграциии с инструментами вроде Delta Lake и Feast (Feature Store);
-- анализ распределений и мониторинг дрейфа данных (data drift), избегаем bias в моделях;
-- кейсы по векторным базам данных и квантовым вычислениям.

DDIA не просто актуальна: она стала ещё важнее с ростом сложности AI-систем.

Но будет ли её новое издание переведено? Думаю, уже нет. Впрочем, и оригинальную версию мало кто разбирал.

Когда в резюме написал
"Создал рабочий проект на FastAPI -- микросервис для работы с моделями машинного обучения"