लो-स्तरीय सिस्टम कोड में Rust सत्यापन तकनीक का उपयोग

 (github.com/verus-lang)
1 पॉइंट द्वारा GN⁺ 2024-05-06 | 1 टिप्पणियां | WhatsApp पर शेयर करें

Rust कोड की सटीकता सत्यापित करने के लिए Verus टूल

  • Verus एक ऐसा टूल है जो Rust में लिखे गए कोड की सटीकता सत्यापित करने के लिए बनाया गया है
  • डेवलपर कोड के लिए अपेक्षित स्पेसिफिकेशन लिखते हैं, और Verus यह स्टैटिक तरीके से जाँचता है कि executable Rust code सभी संभावित रन पर हमेशा उन स्पेसिफिकेशन को पूरा करता है
  • रनटाइम checks जोड़ने के बजाय, Verus एक मजबूत solver पर निर्भर होकर यह प्रमाणित करता है कि कोड सही है
  • Verus अभी Rust के एक subset को सपोर्ट करता है (वर्तमान में विस्तार जारी है), और कुछ मामलों में डेवलपर को standard Rust type system से आगे जाकर स्थिर रूप से कोड की सटीकता जाँचने देता है (उदाहरण: raw pointer manipulations)

Verus की वर्तमान स्थिति

  • Verus अभी तेज़ी से विकसित हो रहा है
  • फीचर टूटे हुए या गायब हो सकते हैं, और दस्तावेज़ अभी भी अधूरे हो सकते हैं
  • Verus को आज़माने से पहले यह मानकर चलें कि आपको Zulip पर मदद के लिए संदेश भेजना पड़ सकता है

Verus का उपयोग करके देखें

  • Verus को ब्राउज़र में आज़माने के लिए Verus Playground जाएँ
  • अधिक जटिल development के लिए, install निर्देशों का पालन करें और ट्यूटोरियल और रेफरेंस से शुरुआत करके नीचे दिए दस्तावेज़ देखें

Verus दस्तावेज़

  • ट्यूटोरियल और रेफरेंस
  • Verus standard library के लिए API docs
  • Concurrency code की verification के लिए गाइड
  • Project goals
  • Verus में योगदान (Contributing to Verus)
  • License

संपर्क करना, issue रिपोर्ट करना और चर्चा शुरू करना

  • यदि आप GitHub पर issue रिपोर्ट करना या discussion शुरू करना चाहते हैं, या रीयल-टाइम चर्चा और मदद की जरूरत हो, तो Zulip में शामिल हों
  • मौजूद फीचरों में वास्तविक executable समस्याओं (bugs) के लिए GitHub issues का उपयोग करें, जबकि फीचर रिक्वेस्ट और planned features पर खुले विमर्श के लिए GitHub discussions का उपयोग करें
  • योगदानों का स्वागत है; यदि आप कोड देना चाहते हैं तो Contributing to Verus के टिप्स देखें

GN⁺ की राय

  • Rust पहले से ही सिस्टम प्रोग्रामिंग के लिए भरोसेमंद और high-performance भाषा के रूप में जानी जाती है; Verus ऐसा लगता है कि यह Rust की इन strengths को और मज़बूत कर सकता है। खासकर concurrency programming verification फीचर बहुत रोचक लग रहा है
  • हालाँकि अभी यह शुरुआती चरण में है और समर्थित Rust grammar सीमित दिखती है, इसलिए इसे सीधे production में लागू करने से पहले अभी और काम लग सकता है। लेकिन स्टैटिक एनालिसिस के जरिए पहले से ही कोड की सुरक्षा सुनिश्चित करना इसलिए बेहद महत्वपूर्ण है, इसलिए इसका भविष्य उज्ज्वल लगता है
  • शुरुआतिक चरण में दस्तावेज़ीकरण की कमी और सीमित syntax support सुधार माँगते हैं, लेकिन लंबी अवधि में यह Rust ecosystem में एक महत्वपूर्ण भूमिका निभाने वाला प्रोजेक्ट लगता है। खासकर systems programming और blockchain जैसे भरोसेमंद क्षेत्रों में इसका उपयोग अधिक हो सकता है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-05-06
Hacker News टिप्पणी
  • Verus का इस्तेमाल करके एक औपचारिक रूप से सत्यापित Kubernetes controller लिखा गया है
    • यह दिखाया जा सकता है कि controller अंततः क्लस्टर को requested desired state तक adjust करेगा, यानी liveness property prove की जा सकती है
    • सही तरीके से specify करने में कई subtleties और nuances हैं (desired state requirements का तेज़ बदलना, asynchronicity, failures आदि)
    • कोड GitHub लिंक पर उपलब्ध है और OSDI 2024 में आने वाले पेपर से लिंक्ड है
  • Verus की दिशा में एक छोटा कदम: Rust में debug_assert से precondition और postcondition जोड़े जा सकते हैं
    • Rust compiler सामान्यतः production build में इन्हें हटा देता है
    • Verus tutorial के उदाहरण और debug_assert से runtime checks के उदाहरण दिए गए हैं
  • "code correctness verification" और "code correctness proof" के बीच अंतर पर एक beginner प्रश्न
    • क्या CS/गणित की पृष्ठभूमि कमज़ोर होने वाले practical programmers के लिए code "proof" सीखने का अच्छा material कहीं उपलब्ध है?
    • "zero-knowledge" proofs क्यों इतने important हैं और क्यों relevant हैं, यह बहुत जानना चाहता/चाहती हूँ
  • Rust standard अभी C/C++, Common Lisp, Ada/SPARK2014 की तरह नहीं है
    • इसी वजह से Ada/SPARK2014 आदि के लिए बने verification tooling के साथ तुलना करने पर यह एक moving target जैसा लगता है
  • Dafny एक "verification-aware programming language" है जो Rust में compile हो सकता है (GitHub लिंक)
  • प्रमुख contributors में से एक ने Zurich Rust meetup में Verus पर बहुत अच्छी प्रस्तुति दी थी (YouTube लिंक)
    • इसमें "ghost" code का program से इतनी clean फिट होना प्रभावित करने वाला था (थोड़ा Ada की याद दिलाता है)
  • Verus और SPARK की तुलना
    • क्या दोनों एक ही class के verifiers हैं? Verus और SPARK में क्या फर्क है, Verus के Ada नहीं बल्कि Rust verifier होने के अलावा?
  • कोई ऐसा व्यक्ति जो Verus में expert है, क्या Verus और Lean4 के performance और expressiveness की तुलना करके बता सकता है?
    • मेरी समझ यह है कि Verus एक SMT-based verifier है और Lean एक interactive theorem prover होने के साथ SMT-based tool भी है
    • लेकिन formal verification में मेरी समझ सीमित है, इसलिए software formal methods में निपुण किसी व्यक्ति की opinion बेहतर होगी
  • Verus और Kani का कोई relation है? या ये अलग तरीके से काम करते हैं? (Kani GitHub लिंक)
  • क्या कोई तरीका है जिससे output code फिर भी एक valid Rust code बना रहे जो vanilla Rust tooling से compile हो सके?