توسعه یک وب‌اپلیکیشن کامل با Lean 4؛ آیا اثبات‌کننده‌های قضیه برای توسعه وب آماده‌اند؟

زبان Lean 4 معمولاً در محافل دانشگاهی و در کنار ابزارهایی مانند Coq و Agda برای اثبات قضایای ریاضی و بررسی درستی فرمال نرم‌افزار شناخته می‌شود. با این حال، هسته اصلی آن یک زبان برنامه‌نویسی تابعی مدرن و قدرتمند با تایپ‌های وابسته (Dependent Types) از خانواده Haskell و OCaml است. اضافه شدن سرور بومی Std.Http به کتابخانه استاندارد Lean در ماه‌های اخیر، زمینه‌ساز این پرسش شد: آیا می‌توان یک وب‌اپلیکیشن کامل و عملیاتی با Lean 4 پیاده‌سازی کرد؟

برای پاسخ به این سوال، پروژه بنچ‌مارک RealWorld (یک کلون از سرویس Medium با تست‌های رسمی API و رابط کاربری) به طور کامل با این زبان پیاده‌سازی شده است.

معماری سیستم و استک فنی

کل معماری پروژه، از بک‌اند تا رابط کاربری، مبتنی بر اکوسیستم در حال رشد Lean پیاده‌سازی شده است:

• سرور و مسیریابی: با تکیه بر Std.Http و کتابخانه lean-routing، مسیرها در جدولی تایپ‌شده تعریف می‌شوند. هماهنگی نوع داده‌های مسیر (مانند شناسه عددی کامنت) با ورودی‌های تابع در زمان کامپایل تضمین می‌شود؛ خطایی که در بسیاری از فریم‌ورک‌های دیگر فقط در رانتایم ظاهر می‌شود.
• پایگاه داده: اتصال به Postgres از طریق leanpostgres (بایندر کلاینت C) و پشتیبانی از Connection Pool انجام می‌شود. ورودی‌های متغیر در کوئری‌ها به صورت پارامترهای مجزا ارسال می‌شوند که امکان هرگونه نفوذ از طریق SQL Injection را در سطح ساختار کد منتفی می‌کند.
• فرانت‌اند هایپرمدیای بدون بیلد: صفحات به صورت Server-side با lean-html رندر می‌شوند. برای بخش‌های تعاملی نیز از کتابخانه نوظهور Datastar و پکیج datastar-lean استفاده شده است؛ رویکردی شبیه به HTMX که بدون نیاز به ابزارهای ساخت پیچیده جاوااسکریپت و بدون فریم‌ورک‌های سنگین SPA، صفحات را در لحظه به‌روزرسانی می‌کند.

نکته جالب این پیاده‌سازی در اختصار آن است؛ بک‌اند Lean تنها با ۱٬۰۳۳ خط کد پیاده شده که در مقایسه با نسخه TypeScript (۱۲۶۷ خط)، نسخه Go (۱۳۷۱ خط) و نسخه C# (۲۳۹۶ خط) فشرده‌تر و گویاتر است.

درستی از طریق ساختار (Correctness by Construction) و هوش مصنوعی

بخش اعظم این کدها با استفاده از ابزار Claude Code و تحت هدایت انسانی نوشته شده است. نویسنده تأکید می‌کند که اتکای صِرف به تست‌ها، به‌ویژه کدهایی که هوش مصنوعی تولید می‌کند، ریسک بالایی دارد؛ زیرا مدل‌ها تست‌های ضعیفی می‌نویسند یا ممکن است شرایط پیش‌بینی‌نشده را لحاظ نکنند.

در Lean می‌توان رفتار برنامه را به‌صورت اثبات‌های ریاضی مستند کرد (Correctness by Construction). برای مثال، نویسنده نوع داده‌ای تحت عنوان Slug تعریف کرده که به شکل رسمی و استقرایی (Inductive) قوانین مجاز بودن آدرس‌های URL را مشخص می‌کند و کامپایلر تا زمان برقراری دقیق این شرایط به کد اجازه اجرا نمی‌دهد.

با این حال، یک تله جدی در استفاده از AI برای زبان‌های اثباتی مطرح شده است: هوش مصنوعی هنگام درخواست اثبات، اغلب سراغ قضایای بدیهی ریاضی می‌رود که ربطی به باگ‌های منطقی برنامه ندارند. بنابراین حتی کدهایی که اثبات معتبر ریاضی دارند، بدون بازبینی دقیق انسانی نباید مورد اعتماد قرار گیرند.

آیا Lean 4 برای محیط پروداکشن آماده است؟

اگرچه تست‌ها با موفقیت پاس شده‌اند، توسعه‌دهنده به چالش‌های جدی پیش از استقرار در پروداکشن اشاره می‌کند:

1. محدودیت کارایی سرور: به دلیل وجود باگی در رانتایم (که رفع شده اما هنوز نسخه عمومی آن منتشر نشده)، سرور HTTP در حال حاضر حداکثر چند هزار درخواست در ثانیه را روی هر پردازش پاسخ می‌دهد.
2. اکوسیستم نوپا: کتابخانه‌های موجود بسیار جوان هستند و اغلب تنها یک یا دو نگه‌دارنده دارند. به‌روزرسانی‌های ماهانه Lean نیز معمولاً شکست‌های ناسازگار (Breaking Changes) ایجاد می‌کند.

پاسخ نهایی نویسنده این است: این نرم‌افزار برای بارهای ترافیکی معقول، به شرط قفل کردن نسخه‌های کامپایلر و ابزارها (Pinning) و بازبینی انسانی دقیق کدهای SQL و بایندرهای C، کاملاً قابلیت استفاده دارد.

بازخورد جامعه مهندسی

در گفت‌وگوهای Hacker News، کاربران این پلتفرم را یک «Haskell ارتقایافته» خواندند که به لطف سیستم تایپ‌های وابسته، برنامه‌نویسی روزمره را حتی بدون نوشتن اثبات‌های کامل ریاضی بسیار لذت‌بخش و ایمن می‌کند. مهندسان حاضر در بحث اشاره کردند با اینکه اکوسیستم وب Lean 4 هنوز راه زیادی تا بلوغ زبان‌هایی چون Go یا Rust دارد، اما استفاده از آن برای ایجاد سیستم‌های دقیق با معماری‌های مدرن وب به‌خوبی قابلیت عملیاتی خود را به اثبات رسانده است.