أُطلقت أداة جديدة تُدعى «Lasm» تهدف إلى إحداث نقلة نوعية في تطوير تطبيقات الويب، وذلك بتمكين المطورين من بناء تطبيقات مُبرهنة رسميًا باستخدام لغة البرمجة «Lean 4». تُحوّل «Lasm» برامج «Lean 4» إلى «WebAssembly» قبل التشغيل، مما يفتح الباب أمام مجموعة واسعة من بيئات النشر.
تسمح هذه الأداة بكتابة قاعدة كود واحدة بلغة «Lean 4» ثم نشرها كخادم «Node»، أو دالة بلا خادم (serverless)، أو دالة طرفية (edge function)، أو وحدة «WASI/Fastly»، أو حتى تطبيق متصفح. هذا التنوع يجعل «Lasm» حلًا مرنًا للمشاريع التي تتطلب تشغيل الكود في بيئات مختلفة.
البرهان الرسمي في صميم التطوير
الميزة الأبرز في «Lasm» هي القدرة على إثبات خصائص الكود الذي يتم نشره بشكل رسمي. يوضح المشروع مثالًا رئيسيًا، وهو تطبيق «Conduit» (نسخة مطابقة لتطبيق «Medium»)، الذي يأتي مع 117 مبرهنة تم التحقق منها. تغطي هذه المبرهنات جوانب حيوية مثل الأذونات، والتتبع، والتفضيلات، والترقيم، وصلاحية المدخلات. تعمل هذه المبرهنات على نفس الكود الفعلي الذي يتم تشغيله، مما يوفر مستوى عالٍ من الثقة في صحة سلوك التطبيق.
بينما تُبرهن «Lasm» صحة منطق التطبيق بناءً على نموذج للجداول، من المهم ملاحظة أن بعض الجوانب تُعتبر موثوقة وليست مُبرهنة رسميًا. يشمل ذلك تنفيذ عبارات SQL، وطبقة نصوص JSON، والتزامن بين الطلبات، بالإضافة إلى الثقة في «Lean» و«Lasm» وبيئة تشغيل «JavaScript» نفسها. التوافق مع مواصفات «RealWorld» الكاملة يتم اختباره، وليس برهنته.
تجربة المطور والتكامل السهل
تتوفر «Lasm» عبر «npm»، مما يسهل تثبيتها واستخدامها. كل ما يحتاجه المطور هو «Node» (أو «Bun» أو «Deno»). تدعم الأداة التوافق مع حزم «npm» وتوفر أدوات بناء سريعة؛ حيث يستغرق البناء الأول حوالي 19 ثانية على بيئة «Linux CI»، بينما تستغرق التعديلات اللاحقة 1-2 ثانية فقط. تدعم «Lasm» أنظمة «Linux» و«macOS» و«Windows» لتطويرها.
يُمكن نشر تطبيقات «Lasm» على مجموعة واسعة من المنصات السحابية والطرفية، بما في ذلك «AWS Lambda»، و«Vercel Functions»، و«Netlify Functions»، و«Azure Functions»، و«Google Cloud Functions»، و«Cloudflare Workers»، و«Vercel Edge»، و«Netlify Edge»، و«Deno Deploy»، و«Supabase Edge Functions»، و«Fastly Compute»، بالإضافة إلى بيئات «Bun» و«Deno» و«WASI».
نرى أن «Lasm» يقدم للمطورين فرصة فريدة لبناء تطبيقات ويب تتسم بموثوقية عالية بشكل لم يكن متاحًا من قبل في عالم تطوير الويب التقليدي. إن القدرة على برهنة صحة الكود رسميًا يمكن أن تحدث فرقًا كبيرًا في التطبيقات الحساسة التي تتطلب دقة متناهية، مما يقلل من الأخطاء المحتملة ويزيد الثقة في الأنظمة التي نبنيها. هذا التوجه نحو التحقق الرسمي قد يصبح معيارًا جديدًا في المستقبل لتطبيقات الويب المعقدة والمهمة.
المصدر: github.com