Разработчик собрал RealWorld на Lean 4 с помощью Claude Code

Автор блога leangineer.com решил проверить, можно ли уже построить настоящее веб-приложение на Lean 4. Этот язык из семейства Haskell и OCaml большинство знает как систему доказательства теорем, но недавно в его стандартной библиотеке появился HTTP-сервер, а сообщество пишет и остальное: драйверы Postgres, криптографию, рендеринг HTML. Для проверки автор воспроизвёл RealWorld, известное эталонное приложение, клон Medium, к которому прилагаются официальные наборы тестов для API и для сайта. Версия полностью написана на Lean, включая фронтенд, а интерактивность даёт datastar-lean. Код выложен на GitHub. Текст оформлен как математическая статья: то, что реально доказано, помечено как предложения (propositions), и Lean проверяет эти доказательства при каждой сборке.

Собрано всё так. Сервер, Std.Http из стандартной библиотеки Lean (там он, по словам автора, с апреля; год в тексте не указан). Маршруты API объявлены таблицей через lean-routing: у каждого пути типизированные параметры и свой обработчик. JSON, lean-json, хеширование паролей через scrypt из OpenSSL, lean-libcrypto, токены входа (JWT), lean-jose, CORS, cookies и статические файлы, lean-middleware. Данные лежат в Postgres: leanpostgres оборачивает клиент на C и держит пул соединений, SQL пишется прямо в коде, а подставленное значение уходит в запрос отдельным параметром, так что пользовательский ввод не может выполниться как SQL; схему применяет leanmigrate при старте. Страницы рендерятся на сервере через lean-html без шаблонов, HTML пишется обычными функциями Lean. Для удаления комментария достаточно обработчика onClick: небольшой скрипт Datastar отправляет DELETE-запрос и обновляет страницу ответом сервера, который строится той же функцией, что и JSON API. Отдельного этапа сборки фронтенда нет. datastar-lean, официальный Lean-SDK для Datastar, его поддерживают автор и Карло Хамалайнен (Carlo Hamalainen). Если собрать три части и прогнать оба набора тестов, они проходят.

По стоимости: бэкенд на Lean занимает 1033 строки, меньше всех из четырёх сравниваемых реализаций (TypeScript, 1267, Go, 1371, C#, 2396). Десять из одиннадцати используемых библиотек написал Пол Бутчер (Paul Butcher); Claude Code и автор отправили исправления в шесть из них.

Дальше автор спрашивает, выдержит ли приложение реальных пользователей. Он называет две проблемы «молодого стека». Первая: HTTP-сервер Lean упирается в несколько тысяч запросов в секунду на процесс, в основном из-за ошибки в рантайме Lean, которая уже исправлена, но ещё не выпущена. Вторая: новые версии Lean выходят каждый месяц и часто ломают библиотеки. Для небольшого сайта с зафиксированными версиями, по мнению автора, ни то ни другое не критично. Третья оговорка, кто писал код: почти ничего не написано вручную, приложение создал Claude Code по указаниям автора, большинство библиотек сделано так же, всему несколько месяцев, у большей части один-два контрибьютора. Поэтому ошибки, которые видны только при реальном использовании, скорее всего, ещё внутри.

Надёжнее всего то, что проверяет Lean: типы и теоремы, независимо от того, кто написал код. Инструкции библиотек для ИИ-агента требуют «сильнейшей формы утверждения» (доказанной теоремы вместо примера) и запрещают sorry как заглушку вместо доказательства; в нескольких библиотеках есть настоящие доказательства. Код, не покрытый теоремами, надёжен ровно настолько, насколько надёжны его тесты, а для привязок к C-библиотекам Lean вообще не проверяет C-код. При этом доказательства нужно читать: Lean проверяет верность доказательства, но не то, что теорема утверждает нужное. Автор приводит эксперимент Дэна Луу (Dan Luu): когда агентам поручили реализовать сжатие Zstd на Lean 4, они в основном доказывали арифметические факты мимо кода, где обычно и бывают баги, и код от этого не стал корректнее. Помочь с чтением может инструмент claimcheck: ИИ-модель пересказывает каждую теорему простым языком, не зная замысла, а затем пересказ сравнивается с исходным намерением, полезно, но чтение не заменяет.

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

Наконец, автор обсуждает «корректность по построению», когда код выводится из формальной спецификации шагами, каждый из которых доказан. Он считает это единственным надёжным способом сохранить скорость, которую даёт ИИ, и не потерять качество. Но у RealWorld формальны только типы (файл OpenAPI), а поведение описано словами и пинится лишь тестами, поэтому приложение не выводилось из спецификации: его сначала написали, затем протестировали. Вместо этого автор выбрал несколько свойств для проверки; три из них гарантированы самим фактом компиляции. Первое: если типы обработчика не совпадают с маршрутом, код не скомпилируется (например, обработчик с id типа String вместо Nat). Слабое место, таблицу маршрутов автор скопировал из файла OpenAPI вручную; автоматическая генерация закрыла бы этот пробел. На примере «слага» (URL-вида заголовка вроде how-to-train-your-dragon) автор показывает принцип в малом: сначала формальная спецификация, тип Valid, исключающий пустые слаги, дефисы по краям и двойные дефисы, затем Slug как строка вместе с доказательством её допустимости. Текст источника обрывается на этом определении, остальная часть раздела о корректности здесь не отражена.

Ключевые факты

RealWorld (клон Medium с официальными тестами API и сайта) целиком написан на Lean 4, включая фронтенд на datastar-lean; оба набора тестов проходят, код открыт на GitHub.
Бэкенд занимает 1033 строки, меньше TypeScript (1267), Go (1371) и C# (2396); всё приложение, около 1600 строк.
Почти весь код написал Claude Code по указаниям автора; десять из одиннадцати библиотек принадлежат Полу Бутчеру, в шесть из них отправлены исправления.
Для реальных пользователей приложение годится при трёх условиях: скромный трафик, зафиксированный тулчейн и кто-то, кто читает код; сервер Lean держит лишь несколько тысяч запросов в секунду на процесс, а новые версии Lean выходят каждый месяц и ломают библиотеки.
Полной «корректности по построению» нет: у RealWorld формальны только типы; три выбранных свойства гарантирует компилятор, например, обработчик с типами, не совпадающими с маршрутом, не скомпилируется.

Почему это важно

Это практический ответ на вопрос, можно ли писать обычные веб-приложения на Lean, который до недавних пор был в первую очередь системой доказательства теорем. Пример показывает, что с HTTP-сервером в стандартной библиотеке и набором сторонних библиотек (Postgres, JSON, JWT, HTML) полноценный клон Medium с сервером, базой и фронтендом собирается и проходит официальные тесты. Вторая линия сюжета, роль ИИ-агента: почти весь код написал Claude Code, а автор обсуждает, что в такой ситуации можно доверить проверке Lean, а что всё равно нужно читать глазами.

Кому это важно

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

Как это применить

Автор сформулировал условия, при которых такое приложение можно выпускать к реальным пользователям: небольшой трафик, зафиксированные версии тулчейна и осознанное чтение кода, в первую очередь обработчиков, SQL и привязок к C. Для большей нагрузки можно запускать несколько копий, поскольку приложение не хранит состояние между запросами. Идея для работы с агентами: просить у них доказанные теоремы вместо примеров, запрещать sorry как заглушку, а доказательства всё равно проверять на содержательность; для этого автор упоминает инструмент claimcheck. Код приложения открыт на GitHub.

Можно ли доверять

Источник, личный блог автора о собственном проекте; имя автора и дата публикации в доступном тексте не указаны. Утверждения о прохождении тестов и о размере кода, слова автора, количество тестов и подробные результаты в тексте не приведены. Скорость сервера обозначена только качественно (несколько тысяч запросов в секунду на процесс), без измерений. Текст источника обрывается на разделе о корректности, поэтому выводы этого раздела здесь не отражены. Автор сам честно отмечает, что код новый, написан быстро и в нём, вероятно, остались ошибки, которые видны только при реальном использовании.

Риски и подводные камни

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

«самая сильная форма, которую допускает утверждение: доказанная теорема о свойстве … а не пример и ожидаемый результат»

— инструкции библиотек для ИИ-агента, как их цитирует автор поста