أنا أعمل على مواصفة Concrete v2. النسخة الأولى لديها كود يعمل بالفعل وتعلمنا الكثير من خلال تنفيذه. الآن أضفت بعض الميزات الجديدة المثيرة للاهتمام التي تأتي من زيغ، أوسترال، لين/كوك. أنا أصمم لغة أنظمة تدور حول التحقق الرسمي من البداية مع بعض الميزات المثيرة للاهتمام. الميزات: - النواة التي تم توثيقها في Lean 4 - الأنواع الخطية (على الطراز الأسترالي، وليس الأفيني الخاص براست) - الاستعارة بدون تعليقات مدى الحياة - قدرات تتبع التأثيرات - تم تمرير المخصص كقدرة (نمط الزيغ) - نقي بشكل افتراضي - ! للدوال غير النقية (من روك) كيف يكونون: الأنواع الخطية هي الأساس. كل قيمة تستهلك مرة واحدة فقط. لا تسريبات، ولا يوجد تسريب مزدوج، ولا فائدة بعد المجانية. أمان الذاكرة بدون وجود بيانات مظلمة. هي أكثر تفصيلا لكنها أكثر وضوحا وواقعية من الأنواع الأفينية. الاقتراض يجعل الخطية قابلة للاستخدام. الإشارة مؤقتا إلى قيمة دون استهلاكها. المناطق المعجمية بدلا من تعليقات Rust مدى الحياة. المترجم يستنتج ما يجعلك Rust تكتب. القدرات تتبع التأثيرات. دالة تقرأ الملفات تعلن ذلك. وظيفة تخصصه تعلن ذلك. لا إعلان يعني لا تأثيرات، مضمون. grep مع (Network) يجد كل وظيفة تلامس الشبكة. المخصص كقدرة يجعل التخصيص مرئيا. كود بدون (Alloc) لا يثبت أنه لا يمس الكومة. أنت تتحكم في أي مخصص يخدم أي مسار كود. ساحة، تجمع، تخصيص المجموعات، كلها صريحة. النسخة النقية بشكل افتراضي تعكس النموذج المعتاد. التأثيرات تتطلب إعلانا. الحالة الشائعة (الحوسبة البحتة) لا تحتاج إلى تعليق. النواة اللينة تربط كل شيء معا. عندما يقول المترجم إن برنامجك آمن، فإن هذا الادعاء مدعوم بإثبات.