F*: प्रमाण-आधारित प्रोग्रामिंग भाषा
मूल शीर्षक: F*: A general-purpose proof-oriented programming language
यह क्यों महत्वपूर्ण है
F* उच्च-आश्वासन सॉफ़्टवेयर सत्यापन में उद्योग-स्तरीय अनुप्रयोग प्राप्त कर रही है, जो सुरक्षा-महत्वपूर्ण प्रणालियों में formal verification को व्यावहारिक बनाती है।
F* (एफ स्टार) एक सामान्य-उद्देश्यीय proof-oriented प्रोग्रामिंग भाषा है जो dependent types, SMT solving और tactic-based theorem proving को एकत्रित करती है। यह Microsoft Research और Inria द्वारा विकसित एक open-source परियोजना है।
F* एक सामान्य-उद्देश्यीय proof-oriented प्रोग्रामिंग भाषा है जो purely functional और effectful दोनों प्रकार की प्रोग्रामिंग को समर्थन देती है। यह dependent types की अभिव्यंजक शक्ति को SMT solving आधारित proof automation और tactic-based interactive theorem proving के साथ जोड़ती है।
F* प्रोग्राम डिफ़ॉल्ट रूप से OCaml में compile होते हैं। इसके अलावा F#, C, Wasm (KaRaMeL टूल द्वारा) और assembly (Vale toolchain द्वारा) में भी निकाले जा सकते हैं। F* स्वयं F* में लिखी गई है और OCaml से bootstrapped है। यह Apache 2.0 लाइसेंस के अंतर्गत GitHub पर उपलब्ध है और Windows, Linux, Mac OS X के लिए binary releases नियमित रूप से जारी होती हैं।
F* का उपयोग कई महत्वपूर्ण औद्योगिक और शैक्षणिक परियोजनाओं में किया जा रहा है। Project Everest इसका प्रमुख उपयोगकर्ता है, जो उच्च-आश्वासन सुरक्षित संचार सॉफ़्टवेयर विकसित करता है। HACL* क्रिप्टोग्राफ़िक primitives की लाइब्रेरी F* में लिखी गई है, जिसका कोड Mozilla Firefox, Linux kernel, Python, mbedTLS, Tezos blockchain, और WireGuard VPN जैसे उत्पादन परियोजनाओं में उपयोग हो रहा है। EverParse, जो binary formats के लिए parser generator है, Windows Hyper-V में उपयोग किया जाता है जहाँ Azure cloud platform से गुज़रने वाला हर नेटवर्क पैकेट इससे parse होता है।
सीखने के लिए "Proof-oriented Programming In F*" नामक ऑनलाइन पुस्तक उपलब्ध है तथा GitHub Discussions और Zulip पर समुदाय सक्रिय है।