مايكروسوفت ريسيرش تكشف النقاب عن F*: لغة برمجة موجهة نحو البرهان
2024-12-25
F* (تنطق إف ستار) هي لغة برمجة عامة موجهة نحو البرهان، تدعم كلًا من البرمجة الوظيفية البحتة والبرمجة ذات التأثيرات الجانبية. تجمع بين قوة التعبير عن الأنواع التابعة مع أتمتة البرهان القائمة على حل SMT وإثبات النظرية التفاعلية القائمة على التكتيكات. تتكوّد برامج F* بشكل افتراضي إلى OCaml. ويمكن أيضًا استخراج أجزاء مختلفة من F* إلى F# أو C أو Wasm باستخدام أداة تسمى KaRaMeL، أو إلى لغة التجميع باستخدام سلسلة أدوات Vale. تم تنفيذ F* بلغة F* نفسها، وتم تمهيدها باستخدام OCaml. F* مفتوحة المصدر على GitHub، وهي قيد التطوير النشط من قبل Microsoft Research و Inria والمجتمع. تُستخدم في العديد من المشاريع، بما في ذلك Mozilla Firefox ونواة Linux، مما يُظهر تطبيقاتها في مجالات الأمن، والتشفير، وتطوير النظم.