Fireship выкатил видео про x402 — протокол internet-native криптовалютных платежей.

Мне очень нравится такая идея, и здесь это реализовано удобнее всего, что я видел.
Протокол не зависит от какого-то конкретного блокчейна, работает по HTTP.
На запрос пользователя можно ответить статусом 402 и страничкой с оплатой. Кому-то может понравиться, что это открывает AI-агентам доступ к использованию денег.

x402 решает кучу проблем по типу нужды в мониторинге блокчейна для подтверждения оплаты, защиты от повтора и связи платёж–контент, что в том числе упрощает UX.
Большую часть этой работы берёт на себя Facilitator — централизованный сервис подтверждения транзакций. В официальном SDK по умолчанию используется Facilitator от Coinbase — разработчиков протокола (легко поменять на другой при конфигурации). Сам протокол сфокусирован на USDC в EVM/SVM сетях (точнее его реализация, но этим не ограничивается).
Поддержку произвольных токенов планируют завезти в Q2 2026.

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

Explorer проектов, принимающих платежи через систему: x402scan

Limit Order Book, он же стакан — механизм биржи, объединяющий покупателей с продавцами.

Исходя из названия, он собирает в себе лимитные заявки. У каждого ордера есть такие параметры как:
- side — всё просто, покупка или продажа.
- quantity — количество актива в заявке.
- price — очевидно, цена.
Про Time in Force и скрытые ордера чуть позже.

Когда мы хотим купить какой-то актив здесь и сейчас, мы отправляем market order на биржу, где её matching engine исполняет его, сопоставив с лимитными ордерами.

Приоритетность исполнения одних лимитных ордеров перед другими зависит от логики конкретного matching engine, но есть некоторые общие правила:
- Price–Time Priority — сначала метчим ордера с лучшей ценой, но если несколько стоят по одной цене, то из них выбирается тот, который был выставлен раньше.
- Price–Pro-Rata Priority — исполняем по лучшей цене, но если на этой цене стоит несколько крупных ордеров, то метчим их пропорционально их объёму.
- Size–Time Priority — на одинаковой цене между ордером с большим объёмом и выставленным ранее выберем тот, у кого больший объём.
- Visibility Priority — Visible > Iceberg > Hidden.

Про видимость ордеров:
- Visible — просто ордера, полностью видны всем участникам рынка.
- Iceberg — ордера, видимые в стакане лишь частично. Когда их заданная видимая часть исполняется, биржа обновляет ордер с новой видимой частью, которая будет максимум заданного в параметрах ордера размера, пока он не исполнится полностью. При обновлении ордер может терять приоритет по времени.
- Hidden — в ордербуке не видны, но трейды по ним исполняются. Можно заметить в виде сделок, которые прошли по непойми откуда взявшейся цене между best ask / best bid.

Time in Force:
- GTC (Good Till Cancelled) — ордер остаётся в стакане, пока его полностью не исполнят или пока пользователь не отменит его.
- IOC (Immediate Or Cancel) — ордер должен быть исполнен немедленно хотя бы частично; всё неисполненное сразу отменяется. Забирает ликвидность, но в отличие от простого Market ордера ставит ограничение на цену, а не просто исполняется по доступной цене.
- FOK (Fill Or Kill) — жёсткая версия IOC. Ордер должен быть исполнен полностью и сразу; если это невозможно — он отменяется полностью.

Поправляйте, может где ошибся

сегодня наконец дописал статью про то как я делал minimodal

контекст: modal.com это очень крутая серверлесс платформа для машинного обучения

было очень много всего сделано - точно такой же sdk, control plane который собирает образы, переправляет запросы воркерам (делать шедулер запросов было очень интимно), воркеры которые исполняют код в изолированных песочницах и возвращают результаты на сокетах. есть и батч операции, и стриминг, и все это вроде должно работать благодаря ретраям, DLQ и circuit breaker
ну и всякие удобные штуки типа секретов, вольюмов и вебпоинтов тоже поддерживаются

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

читаем тут - distributedhatemachine.github.io/posts/modal
не читаем тут - github.com/wtfnukee/minimodal

Lean — насколько я понял, это прям честный функциональный язык программирования, который можно использовать для математических доказательств.

Он решает головную боль с верифицированием доказательства. Вы объявляете все структуры и их свойства, пишите доказательство своего утверждения формально, и если код скомпилировался — ваша теорема / лемма / etc. доказана.

Например, объявление группы — это конкретная структура с полями и аксиомами. В Lean (и mathlib) это уже есть из коробки:

class Group (G : Type u) extends Mul G, One G, Inv G :=
  (mul_assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
  (one_mul  : ∀ a : G, 1 * a = a)
  (mul_one  : ∀ a : G, a * 1 = a)
  (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)

При этом почти всегда писать такое вручную не нужно: в mathlib уже есть готовые структуры (Semigroup, Monoid, Group, Ring, Field, и т.д.) и огромная иерархия, где все свойства автоматически подтягиваются через typeclasses. Если у типа есть [Group G], Lean знает, что у него есть нейтральный элемент, обратные, ассоциативность и может использовать это в доказательствах без явных аргументов.


Проблемы Lean 3 (предыдущая версия)

Основная боль 3 версии была не в логике (она корректна), а в автоматизации и тактиках.

Классический пример — solve_by_elim. Эта тактика пытается закрыть цель, перебирая леммы и гипотезы из контекста с бэктрекингом. Проблема в том, что порядок перебора зависел от внутреннего состояния и структуры контекста

В результате один и тот же корректный код мог:
- проходить мгновенно;
- внезапно падать по таймауту;
- зависать при малейшем изменении окружения;


Похожие вещи были и в других конструкциях: simp, repeat, комбинациях try / first, а также при разрешении метапеременных. Таймауты считались по реальному времени, из-за чего скорость машины и нагрузка влияли на результат. Это не приводило к доказательству ложных теорем, но делало валидный код хрупким, нестабильным и плохо воспроизводимым -- что для формальной математики критично.

А что сейчас
В Lean 4 это решили радикально: язык переписали на самом себе, ввели детерминированную модель исполнения (heartbeats вместо wall-clock time), переработали систему тактик и убрали неявную недетерминированность. В результате одинаковый код теперь либо всегда работает, либо всегда падает — независимо от машины и запуска.

Дока языка

Всех с наступающим или уже наступившим