Разработчик написал RealWorld на Lean 4: бэкенд в 1033 строки
I built the RealWorld app in Lean 4
Энтузиаст создал полноценный клон Medium на Lean 4 — языке, известном как proof assistant. Бэкенд занял 1033 строки (меньше, чем на TypeScript, Go и C#), фронтенд тоже на Lean с Datastar. Приложение проходит официальные тесты RealWorld, но автор предупреждает: стек молодой, HTTP-сервер ограничен, а код в основном сгенерирован Claude Code, поэтому требует ручной проверки.
Почти весь этот код написан не вручную. Claude Code написал приложение под моим руководством. Большинство библиотек созданы так же. Всему этому несколько месяцев. У большинства из них только один или два контрибьютора. Код, написанный так быстро, ещё не имел многих читателей или пользователей. Так что ошибки, которые находятся только в реальной эксплуатации, вероятно, всё ещё там.