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

В 2023 году токен TITAN (на базе ERC-20) потерял $2 млн из-за ошибки в кастомной функции transferFee. А моя верификация на 100 строк её уже сейчас ловит.

Lendf.Me (ERC-20) был взломан на $25 млн из-за reentrancy в обновлённой логике.

Сейчас активируются атаки ERC-20 "approve race",

и это только всего лишь ОДИН простейший крипто-протокол!

=

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

И я уже, честно говоря, думаю, что зря сделал первый курс по HoTT со всеми исходниками открытым моим курсантам, и всего за 50 долларов.
Видите же, какую золотую жилу 💰 раскопал )
Пожалуй, повышу цену для начала в джва раза, и скидок никаких для этого трека не будет. И дальше цена будет только расти по мере того, как я буду эти изумрудные зёрна отыскивать по темке формальной верификации на базе хотт.

Хотя конечно ключевая фишка не в коде, а в методологии, а ещё точнее, в моей черепушке.

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

Вопрос из мейнстрима: но почему всю эту верификацию не сделать просто обычными тестами?

Главное, что тестирование проверяет, что программа работает правильно на конкретных тестовых случаях.
Например, можно проверить, что Diffie-Hellman вычисляет общий ключ правильно для фиксированных g, p, a, b.

HoTT -- это доказательство. Оно гарантирует, что программа работает правильно во всех возможных сценариях .
Например, можно доказать, что общий ключ в Diffie-Hellman всегда совпадает, даже если злоумышленник перехватывает сообщения (через Path-типы и HomSpace).

=

Тестирование плохо справляется со структурными инвариантами (например, проверка, что вектор всегда имеет длину n).

Я же могу закодировать такие инварианты в типах:

vector = Pi(domain=int, codomain=lambda n: list, function=lambda n: [0] * n)

=

Тестирование требует ручного написания проверок для каждого случая.

HoTT позволяет использовать автоматические методы (например, SMT-солверы, Z3 с моего курса) для доказательства сложных свойств. Она позволяет моделировать атаки через Path-типы и проверять их невозможность.
Например, можно доказать, что злоумышленник не может создать ложный общий ключ, через Sigma-типы для доказательства корректности шагов протокола.

=

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

HoTT позволяет моделировать криптографические примитивы через зависимые типы. Например, я могу определить тип EncryptedMessage, который гарантирует, что сообщение не может быть декодировано без ключа:

EncryptedMessage = Sigma(domain=str, codomain=lambda m: not is_decodable(m), first=message, second=True)

=

HoTT -- это выход на уровень формальных математических методов , где:
-- cвойства доказываются, а не проверяются;
-- структуры данных и их инварианты моделируются на уровне типов;
-- возможны автоматические доказательства и формальный анализ атак.

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

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

It has four built-in logics:
- a probabilistic, relational Hoare logic (pRHL);
- a probabilistic Hoare logic (pHL);
- an ordinary (possibilistic) Hoare logic (HL);
- an ambient higher-order logic for proving general mathematical facts and connecting judgments in the other logics.

Какие минусы в сравнении с моим подходом:

-- В HoTT равенство -- это гомотопия (путь между типами), что позволяет легко и просто формализовать инвариантность и эквивалентность структур (хотим доказать, что два протокола (реализации) "эквивалентны" в смысле безопасности).
Например, в EasyCrypt доказательство того, что a+b=b+a для целых чисел, требует явного аксиоматического подхода. А в HoTT это следует из свойств абелевых групп (коммутативность встроена в структуру).


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

HoTT позволяет инкапсулировать эти условия в зависимые типы: можно определить тип SecureProtocol, который автоматически требует доказательства свойств безопасности.
Например, HomotopyGroup(Protocol, 1) ≡ 0 для первой гомотопической группы.


-- EasyCrypt работает с конкретными алгоритмами и их реализациями.

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


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

=

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

И тут кстати большой вопрос, а насколько эти сервисы сами верифицированы в плане своей реализации? :) А если там программный баг, или ошибка в логике?

У меня по крайней мере логическая реализация HoTT проверяется тестами и стандартным чек-листом просто по "Homotopy Type Theory: Univalent Foundations of Mathematics". А возможно кстати, сделаю формальную верификацию и моей реализации, в качестве хорошего примера.

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

Прувер Tamarin -- a security protocol verification tool that supports both falsification (attack finding) and unbounded verification (proving) in the symbolic model. Security protocols are specified as multiset rewriting systems and analyzed with respect to temporal first-order properties.

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

Кусочки универсальной алгебры, символьные вычисления первого порядка, состояния моделируются через логические формулы (например, в SMT-солверах или в BDD), стандартный модел-чекинг, процесс-алгебры (π-исчисление, ...),.

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

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

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

Казалось бы, ну что, я умнее академиков что-ли, что я это понимаю, а они нет?
Тут сермяга в том, что я смотрю на это с точки зрения опыта и программной инженерии,
а у них это просто классика фейлов стартаперства, любой миддл знает: взялись пилить проект, особенно если он сложный и наукоёмкий, а потенциальные архитектурные ограничения проявились, только когда половина бюджета освоена и поздняк метаться. И "правильно было бы переписать всё заново с нуля" :)
Cобственно выбор хаскеля 💯⛔️

Мой же инсайт, что лучше всего получается на питоне, а начинал я это делать вообще на php, и альфа-версия на сайте работает :)


— Tamarin ограничен моделью маркированных графовых автоматов LTS, сети Петри и т.п., где переходы между состояниями описываются одномерными правилами перезаписи. Сложные структуры (например, гомотопии) требуют ручной абстракции.
— HoTT через высшие индуктивные типы позволяет моделировать многоуровневые переходы и гомотопические пути между состояниями, что особенно полезно для проверки свойств с топологической природой (криптографические протоколы с нелинейными взаимодействиями...).

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

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

— В Tamarin для доказательства эквивалентности требуется явно моделировать обе версии протокола и сравнивать их поведение.
Унивалентность HoTT позволяет легко и просто доказывать эквивалентности между структурами (например, между двумя версиями протокола, если они изоморфны).

— Tamarin работает с формальной общей логикой (AC, ассоциативность, коммутативность), но не поддерживает абстракции высшего уровня.
HoTT позволяет напрямую моделировать сложные математические объекты (группы гомотопий, усечения типов...). Во многих протоколах используются алгебраические структуры (Diffie-Hellman, билинейные формы) или топологические свойства (многомерные состояния...).

Резюме:
Tamarin эффективен для автоматизации проверки стандартных протоколов.

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

(потерпите, немного додумать осталось :)

Наконец, ProVerif: символьный подход к анализу протоколов, аналогично Tamarin, но с акцентом на автоматизированное рассуждение о криптографических свойствах. База -- типизированное расширение пи-исчисления с криптографией, язык моделирования параллельных процессов...
Криптографические примитивы (шифрование, хэширование, подписи) моделируются через функции и уравнения. Символьная модель криптографии Долева-Яо, клаузы Хорна (привет, Пролог), по сути абстрактные методы анализа, которые авторы сами придумали:)
Сложные структуры данных (например, вложенные списки или рекурсивные типы) требуют ручного моделирования.

=> ProVerif будет более практичным -- для автоматического анализа криптографических протоколов в символической модели.

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

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

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

=

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

Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.

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

Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на Lean или Isabelle, кстати и на F*, но их формальные теории как я рассказал ↑ ↑ ↑ сильно проигрывают HoTT (вообще, Воеводский абсолютный гений computer science), а их экосистемы, по достаточно очевидным причинам, или совсем хиленькие или откровенно отстойные.

А вот связка Python (суперинженерная экосистема, с мощной поддержкой и символьных вычислений, и солверов, и функциональщины, и машинлёнинга...)
+ HoTT просто как маленькая библиотечка, получается просто огонь 💥

Посмотрите, какая будет возня если используете Coq + Galline :)
"Формальная верификация смарт-контрактов во фреймворке ConCert"

Но я с этим связываться точно не буду 💯
потому что, ну кто там заказчики догадаться несложно.
Например SELinux верифицированное ядро делалось по заказу Агентства нацбезопасности США. Верификация кода, криптоалгоритмов из этой же серии. Всяческий ЦэБэ или ГазМяс от них тоже недалеко ушёл.

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

C другой стороны связываться с чистой криптой мне просто физически противно 🤮

Как вариант крипто-игры
By 2026, the market for blockchain gaming is anticipated to have grown to $70 billion, an exponential growth rate.
но там ведь тоже каждый второй -- это гэмблинг кал 💩

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

...

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

Придумал в процессе написания!!1 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.

Заключительный пост сериала будет про это.

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

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


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

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

Думайте.

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

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

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

Дорогие боссы, БАЗА: подчинённые вас в 100% наёбывают (и в принципе в 98% правильно делают, и я учу и буду продолжать, как это делать правильно, но это другое). Вешают вам лапшу насколько это трудно, сроки говорят с запасом в 2-5-11 раз, а вы мямлите "ммну ладно"...

Вот что должно быть в вашей команде в первую очередь, если у вас не было опыта сеньорства:

Программисты должны еженедельно мучительно доказывать КАЖДЫЙ стори-поинт на общем собрании.

Не знаете что это, спросите жпт.

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

Причём это не то что "а давайте Олегу дадим три пойнта, а Оксане пять", нет.

Даже одно очко должно быть ОЧЕНЬ трудно получить :)

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

Не бойтесь, сегодня никуда разработчики не разбегутся, покряхтят и начнут работать как надо.

А вам, программисты, надо быть Человеками прежде всего (с капиталистами-то всё ясно, они по дефолту идут в ад). А не то...

С одной стороны, эту тему я немного продумал, получается топчик. Даже совсем детский пример "сделать игру три-в-ряд" на моём hott-движке, вот как можно подходить к проектированию, навскидку:

-- в архитектурном плане это State Machine (n-мерный тор) на основе гомотопий с поддержкой обмена сообщениями (гомотопии на поверхности тора описывают переходы между состояниями);

-- доска (GridState, состояние сетки 8x8) -- точка в пространстве, переходы между которыми моделируются гомотопическими путями (ходами игрока);

-- спецэффекты(например, удаление всех элементов одного типа) моделируем высшими индуктивными типами (базовые точки как активация бонуса, и пути, влияющие на GridState);

-- комбинации из 3+ одинаковых элементов в рядах/столбцах -- гомотопический инвариант (группа), автоматическая трассировка для обнаружения эквивалентных конфигураций;

-- подсчёт очков -- дискретная точка без внутренней структуры (TruncationLevel.0). Принцип унивалентности позволяет легко и просто менять эквивалентные сценарии (например, разные комбинации с одинаковой стоимостью);

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

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

мы со святым Робертом Милнером (автор LCF, ML-языки, пи-исчисление...) визуально стали почти неотличимы, и это радует :)
смиренно преклоняюсь к трудам гуру как к его стопам 🙏

...Более того, у многих не получается создать что-то работающее даже просто в модели обмена сообщениями (база: изучайте akka, erlang, ну и формальную логику ↑↑↑ :)

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

Признаю, это полностью моя недоработка 💯
как закончу второй курс по гомотопической теории, плотно прям берусь за доработку практики ООАП, забустим её моделью акторов Хьюитта.

HoTT же, думаю, останется навсегда лишь для самых умненьких (только 0,002% способны.... :).

=

Software/System Design -- это про то что вне зависимости от объёма вашего проекта у вас обязательно там и тут будут образовываться big balls of mud конкретно в вашем коде. И тут важно эксплицитно разделять три типа этого дерьма:

-- DevOps и System Design in Large: бесконечные архитектурные боли и страдания , связанные с интеграцией чужих каках (все эти опенсорсные либы, микросервисы брокеры балансировщики очереди куберы-шмуберы), подчас вообще чистый devops, который сегодня стало модным скидывать на чистых разработчиков;


-- System Design in Small: технические возможности кривейшие ограничения, накладываемые фреймворком, все эти MVC ORM...


-- Software Design/Programming in Large: наконец, собственно программный код, ключевая мякотка везде и всегда. Вы никуда не уйдёте от того, что в абсолютно любом крупном проекте обязательно будут сотни-тысячи сущностей, как их не обзывай (типы данных, классы, таблицы базы..), и вам придётся как-то увязывать (скорее всего асинхронную) логику их работы.

Я делал и буду делать акцент только на этом пункте, трек ООАП ровно про это. Девопсу и SD вас научат сегодня в любой подворотне, потому что это то что можно в проекте "пощупать", а вот PiL фактически нигде не найти (слишком абстрактно, примерно как рефакторинг для менеджеров).

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

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

Посмотрите легендарный тред " Dwarf Fortress source code":
the source code is so mind-buggeringly complicated and idiosyncratic that nobody else except Toady can really understand it

Тут ведь самое важное вот в чём: не запутаться в первых 16, 64, 256, 1024-классах, причём первые 2-3 шага ключевые. Хочу продемонстрировать вживую и, главное, "научать", как можно с самого начала и на всю перспективу удерживать линейной сложность программного кода с логикой взаимодействия тысяч типов сущностей в реальном времени даже для неоднозначного и нечёткого ТЗ с постоянными новыми хотелками.

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

Дон Хуан из микрософта классный пост:

"Грядущая революция искусственного интеллекта в распределённых системах"

Как AI создал точные формальные спецификации TLA + из исходного кода Azure Storage, и затем выявил тонкий баг, который не сдавался классическим code review и тотальному тестированию.

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

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

И с твоим проектом в итоге либо всё будет хорошо, либо нет. Одно из двух.

.

"Всё что нужно знать про Entity-Component-System"
(геймдев открывает для себя функциональное программирование:)

Ну, да, для системы с тысячами типов данных, как dwarf fortress, ECS + реляционная модель, "усиленная" джсонами.

Связи через графовые отношения:

Гном (id=123) держит меч (id=456) из обсидиана (id=789) =>
CREATE (:Сущность {id:123})-[:HOLD]->(:Сущность {id:456})-[:MADE_OF]->(:Материал {id:789});

Да вот только тривиальное "найти всех гномов в радиусе 10м, держащих деревянный меч", систему сразу подвесит :) Я бы ещё для хардкора DDD накинул, чтобы только первичные требования составлять пару лет (и через месяц реализации понять, что надо было делать совсем по другому).


-- Реактивщина + стрим процессинг?

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


-- Онтика? RDF/OWL?

:Лава rdf:type :МагматическийМатериал ;
        :hasReaction [:with :Вода ; 
                      :produces :Пар, :Обсидиан] .
:Гном :можетДержать :Предмет .

+ SPARQL-ом "найти материалы, которые ржавеют при контакте с водой"

Пихаем всё графом в Neo4j...

да только оверхэд на инференс в реалтайме получаем уже на первых 50 сущностях :)

Разве что на Rust + Bevy пилить, да тут сам загнёшься соответственно от когнитивный перегрузки.

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

-- На виртуально бесконечных ресурсах я бы выбрал скорее всего Event Sourcing + CQRS, тут не просто отладка элементарная, а мы вообще получаем по сути детерминированную машину времени, и решаем кучу проблем.

Собственно вот:
Domain-Driven Design: The Power of CQRS and Event Sourcing

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


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

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

Линзы кстати неплохая темка: когда мы фокусируемся на части структуры данных (своеобразная инкапсуляция геттеров и сеттеров в одной сущности).

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

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

-- Рефлексивное описание дварфа
dwarfSchema :: ReflectiveSchema
dwarfSchema = ReflectiveSchema
  { _fields = 
    [ ReflectiveField "name" stringLens [notEmpty] "Dwarf name"
    , ReflectiveField "health" healthLens [range 0 100] "Health points"
    , ReflectiveField "skills" skillsLens [validSkills] "Skill levels"
    ]
  , _relationships =
    [ Relationship "belongsTo" "fortress" fortressIdLens
    , Relationship "hasMany" "items" itemsLens
    ]
  }

-- Динамическое построение запросов
buildQuery :: String -> Query
buildQuery "dwarf.skills.mining > 10" = 
  Query $ dwarfSchema ^. field "skills" . field "mining" . filtered (> 10)

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

На хаскеле это всё красиво выглядит, но страшно далёк он от трудового итэ-народа.

Почему SaaS сегодня -- это проигрышная бизнес-модель?

Чтобы заключать крупные сделки, нужны корпоративные продажи (организовать такой процесс крайне тяжело), продвинутая техподдержка, постоянная кастомизация -- все те скучные и не требующие обслуживания вещи, с которыми так хорошо справляются Яндекс и Мэйл. Ещё в девяностые был случай, знакомой накодил опердень и ходил соло ставил по банкам триал на 60 дней. В одном банке триал закончился, а у них уже работа на нём ведётся, ему звонят "срочно!", он говорит "ну так надо же оплатить", после чего к нему приехали хмурые пацаны в кожаных куртках и сказали: финансовыми вопросами разбирайтесь сами, но банк должен сегодня заработать :)
Сегодня это впрочем стало цивилизованно: юристы просто придушат, и будешь по жизни поддерживать свой SaaS для таких забесплатно.

=

Если же будете ориентироваться на клиентов поменьше, то быстро поймёте, что SaaS -- это буквально гонка на выживание. Сегодная AI + low/no code развивается так быстро, что условный ООО/ИП 100500 раз подумает, стоит ли вкладывать в ваш продукт 10,000 рублей, вместо того чтобы за 2,000 рублей взять подписку на Клода 4, который сразу закодит 80% требований, или купить более дешёвый клон вашего продукта, который какой-то студентик запилил за 48 часов.

=

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

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

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

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



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

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

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


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

39. Жёсткий хейт SOLID | ISP (СильныеИдеи++)
Версия происхождения ISP такая, что дядюшка Боб много-много лет назад консультировал Xerox, и захейтил "God object" (это когда в один объект понапихали кучу всего), выступив в качестве Кэпа Очевидность. У них был некий божественный объект Job, и вот Мартин предложил просмотреть все места в коде, где он используется, для каждого такого места посмотреть, какая группа схожих методов там применяется, и выделить их в промежуточный интерфейс...

За 45 лет ИТ-карьеры я не видел НИ ОДНОГО программиста, кто [...] и при этом не имел бы профессиональных и финансовых результатов.


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


=

Новые материалы для курсантов.

В раздел "Элитный программист" добавлен материал
67) Лучший хак продуктивности.
Мы часто перегружаем свой день, пытаясь быть продуктивными и сделать больше дел. Вместо этого тебе надо ...

=

Курс "Гомотопическая теория типов для программистов (2)": этим летом курс 💯 будет готов.
Закончил универсумы (формальное понятие типа, иерархии, полиморфизм и произведение универсумов, пространство функций...).
Всё это детально разбираем на питоне, и останется домоделировать унивалентность и эквивалентность типов. Потом добавлю кубическую теорию третьим курсом. По увлекательности и глубине с этими темками никакие шахматы или паззлы вроде baba is you и близко не сравнятся.

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

В частности, спустя четыре года вернулся к курсу "Ясная архитектура" — потому что сегодня для программистов владение архитектурными стилями становится едва ли не важнее, нежели само программирование!
На том курсе мы разбираем 13 "клиент-серверных" стилей на практике, с работающим кодом, от хипстерской говноархитектуры, классической процедурщины и объектщины, далее функциональная архитектура, Functional Core / Imperative Shell, Stateless-архитектура (как правильно избавляться от мутабельности), обычный DI, два вида функциональной инъекции, очереди на десятки тысяч rps, архитектура на монадах состояний и т.д.
Добавлю ещё штук пять стилей, включая упоминавшиеся, этим летом 💯