عن المشروع

Takibi هو نموذج بحثي أولي يتكون من لغة أنظمة مخصصة ونواة متجانسة مقابلة لها. يهدف المشروع إلى القضاء على الإخفاقات الشائعة على مستوى النواة - مثل تجاوز سعة المخزن المؤقت، وتسرب الموارد، وانتهاكات السياق - من خلال ترميز هذه الالتزامات مباشرة في نظام الأنواع. تشمل الميزات التقنية الرئيسية ما يلي: - تصميم اللغة: تنفيذ أنواع التحسين (refinement types) لمؤشرات المصفوفات المثبتة، والملكية الأفينية والخطية لإدارة الموارد، ونظام تأثيرات لتتبع سياقات التنفيذ (على سبيل المثال، سياقات الحظر مقابل سياقات المقاطعة). - المترجم: مكتوب بلغة OCaml ويستخدم LLVM 19 لتوليد الكود الأصلي. - قدرات النواة: النواة متوافقة مع Linux-ABI، مما يسمح لها بتشغيل ملفات AArch64 ELF الموجودة. وهي تدعم مجموعة فرعية من نداءات نظام Linux، وجداول الصفحات التي تنمو عند الطلب، والنسخ عند الكتابة (copy-on-write)، ونظام ملفات جذر ext2. - الشبكات: تتضمن مكدس TCP/IP خاص بها يدعم ARP و IPv4/IPv6 و ICMP و TCP. - دعم الأجهزة: يتم الإقلاع على QEMU/AArch64 و Raspberry Pi 5، وهي قادرة على تشغيل Alpine BusyBox وتقديم الملفات عبر HTTPd. يعمل المشروع كوسيلة بحثية لاستكشاف كيف يمكن تطوير لغة لحل مشكلات برمجة الأنظمة في العالم الحقيقي، والانتقال من مصائد وقت التشغيل نحو إثباتات ثابتة للصحة.