यह एक अच्छी पोस्ट है। मैंने पहले program verification किया है, और उस नज़रिए से Rust आधुनिक भाषाओं में formal techniques लागू करने के लिए सबसे उपयोगी भाषा लगती है।
Rust के rules ऐसे कई मामलों को हटा देते हैं जिन्हें formalize करना मुश्किल होता है। बची हुई बड़ी समस्या thread दृष्टिकोण और Rc/borrow दृष्टिकोण से deadlock analysis की है, और ये दोनों कुछ हद तक समतुल्य हैं। अगर Rust में static deadlock analysis हो, तो safe dereference pointers भी संभव हो सकते हैं, और अगर यह साबित किया जा सके कि सभी borrow/upgrade calls विफल नहीं होंगे, तो ज़्यादातर reference counting हटाई जा सकती है। तब जहाँ संभव हो, interior mutability भी लगभग मुफ़्त में मिल जाएगी।
theorem provers की बड़ी समस्या यह है कि उन्हें theorem prove करना पसंद करने वाले लोग बनाते हैं, इसलिए वे formalism में फँस जाते हैं और programmers तथा UI की समझ से उनका तालमेल बिगड़ जाता है। ज़्यादातर proof obligations को SAT solver से संभाला जा सकता है, लेकिन कठिन समस्याओं के लिए भारी tools चाहिए। Coq बहुत ज़्यादा manual है, और लेखक के हिसाब से ACL2 बहुत functional है। machine learning theorem provers को दिशा देने में मदद कर सकता है। proof खुद उससे कराना कठिन है, लेकिन control flow और data usage में मोटे तौर पर समान code से proof plan infer करना संभव लगता है
F* उस मिथकीय भाषा के काफ़ी करीब है जो अपने-आप proofs कर देती है। यह SAT से अधिक शक्तिशाली SMT solver का उपयोग करती है, और अगर automatic solving विफल हो जाए तो manual proof भी संभव है।
Firefox और Wireguard के crypto routines Rust में नहीं, बल्कि F* में—और अधिक सटीक रूप से F* में एम्बेड किए गए low-level DSL Low* में—लिखे गए थे, और वे पूरी तरह verified हैं। https://project-everest.github.io/ https://mitls.org/
सहमत हूँ, लेकिन मेरा मानना है कि Lean अपने समृद्ध metaprogramming features की वजह से interactive theorem proving के user experience में काफ़ी प्रगति कर रहा है।
Rust जैसी किसी बाहरी भाषा के verification में ऐसे tools लागू करने की समस्या यह है कि proofs target language में नहीं लिखे जाते, इसलिए developers को दो भाषाएँ सीखनी पड़ती हैं। Creusot लिखने के अनुभव, Verus और Aeneas पर काम, और Why3 lab के अनुभव के आधार पर मैं सोचता रहा हूँ कि “verification-aware Rust” कैसा दिखेगा। अगर ऐसी भाषा शुरुआत से बनाई जाए, तो verification ease में यह Rust से भी चरणबद्ध रूप से बेहतर हो सकती है, खासकर proof के कठिन हिस्सों में इसका असर बड़ा हो सकता है
लगता है Coq/Agda/Lean परिवार proof के क्षेत्र का विजेता बनेगा। interaction feedback loop के रूप में काफ़ी अच्छा मॉडल है, और ये पहले से मौजूद, वास्तव में काम करने वाले systems हैं।
built-in features में जो चीज़ सबसे ज़्यादा खलती है, वह “मेरे proof पर quickcheck चला दो” जैसी सुविधा है। जब आपके पास code हो और आप किसी ऐसी property को prove करने की कोशिश कर रहे हों जो वास्तव में सही नहीं है, तो proof क्यों नहीं हो रहा यह समझते-समझते सिर पकड़ना पड़ सकता है। अगर proof के बीच में कोई बेमतलब state आ जाए, तो “यहाँ से counterexample generate करो” जैसा command counterexample दे दे, तो अच्छा होगा। proofs बहुत path-dependent होते हैं और आम तौर पर आसान नहीं होते, लेकिन ये tools महानता के बहुत करीब लगते हैं। code को prove करने की प्रक्रिया में यह संभावना भी शामिल होनी चाहिए कि उस code में bug हो सकता है
यह विचार दिलचस्प है कि machine learning theorem prover को guide करे। अगर machine learning system सही निकला, तो वह valid proof तक ले जाकर बड़ा फ़ायदा देगा, और अगर गलत निकला, तो भी बहुत नुकसान नहीं होगा।
prover कोई गलत proof नहीं निकालेगा; वह सिर्फ valid proof निकालने में विफल होगा। ऐसे गुण वाले machine learning applications ज़्यादा नहीं हैं
मैं formal verification का विशेषज्ञ नहीं हूँ, लेकिन मेरा मानना है कि पारंपरिक अर्थों में lock ज़्यादा मददगार नहीं हैं। कोई compiler locks के बारे में वास्तव में उपयोगी कुछ नहीं दे पाता, और बस जोखिम को स्वीकार करके जीना पड़ता है।
वास्तव में Rust में locks और reference counting runtime constructs हैं। Arc Rust के RAII model को काफ़ी हद तक तोड़ देता है, इसलिए scoped threads को हटाना पड़ा, जिनमें scope खत्म होने से पहले destructor चलना चाहिए था। global reference counting में cycles और leaks की समस्या है, इसलिए यह फिर से एक global समस्या बन जाती है। इसे पूरी तरह हटाना मुश्किल होगा, लेकिन मेरा मानना है कि इसे arena-style scopes में सीमित करना बेहतर है। locks की जगह channel जैसे asymmetric data structures ज़रूरी लगते हैं। Go में channel को sender और receiver में बाँटा जाता है, और sender goroutine में defer close(ch) लगाया जा सकता है; panic हो जाए तब भी बाकी thread खत्म होने पर इसका चलना सुनिश्चित होता है। ज़रूरी नहीं कि वह channel ही हो, लेकिन read-write / producer-consumer भूमिकाएँ अलग कर देने से reasoning बहुत आसान हो जाती है और formal analysis में भी मदद मिल सकती है।
यह अच्छा लगा कि बात Hoare के लगभग 1973 के पेपर के उद्धरण से शुरू होकर अब दूसरी पोस्ट तक पहुँची है। मैंने पहले boat की पोस्ट के HN थ्रेड में एक लंबी टिप्पणी लिखी थी कि उस उद्धरण को Rust-केंद्रित नज़रिए की ओर झुकाना, boat की पृष्ठभूमि को देखते हुए समझ में आता है, लेकिन इससे Hoare की आलोचना का दायरा कृत्रिम रूप से संकरा हो जाता है
अब Grayson ने उसी संकरे हिस्से को शुरुआती बिंदु बनाकर Rust के कुछ दिलचस्प क्षेत्रों और design points पर चर्चा की है। मुझे अब भी लगता है कि मेरी टिप्पणी सही थी, लेकिन Grayson की पोस्ट से निकली चर्चा उस मूल पोस्ट के बारे में मेरी तकनीकी शिकायतों की भरपाई करने के लिए काफी थी
1990 के दशक के मध्य तक Hoare खुद भी यह समझ चुके थे कि 1970 के दशक वाले soundness-केंद्रित approach की बुनियाद में कुछ गड़बड़ हो सकती है: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
उसके बाद, साधारण testing से आगे बढ़ी unsound techniques आने लगीं, और मुझे लगता है कि unsound methods sound methods से आगे निकल गए
1973 आज से 50 साल पहले था, यानी किसी विशेषज्ञ के पूरे करियर के बराबर। Hoare सचमुच बहुत करीब पहुँच गए थे
उन्होंने समस्या पहचान ली थी, और पीछे मुड़कर देखें तो type system के ज़रिए shared XOR mutability को enforce करने वाला हल बस एक छोटा-सा कदम लगता है। अगर तब समझ आ गया होता कि वही छोटा कदम असल समाधान है, तो 50 साल की भारी पीड़ा कम हो सकती थी
boat द्वारा Hoare पेपर के उद्धरण पर मैंने मूल रूप से यह सोचा था। Hoare के पहले उद्धरण और छोटे परिचय के बाद लेखक कहता है, “जब Tony Hoare ने कहा कि references jumps की तरह हैं, तब वह mutable और aliased state की समस्या की बात कर रहे थे।” withoutboats एक प्रसिद्ध Rust developer हैं, इसलिए यह व्याख्या चौंकाने वाली नहीं है
लेकिन उद्धरण खुद इस दृष्टिकोण को मज़बूत करता हुआ नहीं लगता। इसे यूँ भी देखा जा सकता है कि Hoare के references के semantic अस्तित्व पर अधिक सामान्य विलाप को लेकर उसे Rust के non-aliased mutable state model पर लागू करके समस्या को bypass करने की कोशिश की जा रही है। पर यह ज़्यादा से ज़्यादा बड़ी समस्या के एक संकरे हिस्से को ठीक कर, फिर यह कहने जैसा है कि पूरी समस्या गायब हो गई। जो हिस्से छोड़ दिए गए हैं, खासकर “Variables” खंड की शुरुआत और ALGOL 68 का उदाहरण, वे इस ओर कहीं अधिक मज़बूती से इशारा करते हैं कि Hoare केवल mutable state नहीं बल्कि reference नाम की semantic concept की ही आलोचना कर रहे थे। मैं मानता हूँ कि Rust समस्या के एक हिस्से को काबू में लाने की कोशिश है, लेकिन मैं नहीं मानता कि किसी भी भाषा ने इस समस्या को “ठीक” कर दिया है
मुझे समझ नहीं आता कि इस पोस्ट की इतनी प्रशंसा क्यों हो रही है। ऐसा लगता है जैसे program analysis के कई पूरे क्षेत्रों को एक ही पैराग्राफ़ में समेट दिया गया हो। मुझे Graydon पसंद हैं और मैं उनके दृष्टिकोण का सम्मान करता हूँ, लेकिन यह पैराग्राफ़ बहुत ज़्यादा simplification करता है
यह कहना कि GC वाली भाषाओं में मज़बूत local reasoning support नहीं होता, एक strawman है। Pony जैसी भाषाएँ रही हैं जो type system में regions रखती हैं और फिर भी GC इस्तेमाल करती हैं। इसके अलावा pointer analysis और escape analysis जैसे पूरे क्षेत्र हैं, जो uniqueness infer करते हैं और तय करते हैं कि क्या दो references aliases हो सकते हैं। Static typing का एक केंद्रीय तत्व भी यही है कि classes और fields जैसी तकनीकों से heap को ऐसे हिस्सों में बाँटा जाए जो एक-दूसरे के alias न हों। बात JavaScript की नहीं है; ऐसा दिखाना ठीक नहीं कि Java/C#/Scala और अनगिनत GC भाषाओं में mutable state पर local reasoning नहीं होता
सामान्य मामले में यह काम पूरी तरह अपने-आप नहीं किया जा सकता, और व्यवहार में separation logic से काफ़ी मिलती-जुलती किसी चीज़ की ज़रूरत पड़ती है। Rust की borrow-checking semantics को भी separation logic के सरल रूपों में से एक माना जा सकता है
classes और fields mutable state पर पूरी local reasoning नहीं देते। क्योंकि class/object A, class/object B की mutable state पर निर्भर हो सकता है। Java-शैली की class inheritance भी समय के साथ program के evolve होने पर अपने-आप और जटिलता जोड़ती है
Graydon यह नहीं कह रहे थे कि GC मज़बूत local reasoning को असंभव बना देता है। उनका कहना यह है कि किसी भी कारण से ज़्यादातर language designers ने ऐसे चुनाव किए जो उस लक्ष्य के विपरीत थे, और यह बात साफ़ तौर पर सही लगती है
बेशक counterexamples हैं, लेकिन अगर Java, C#, Python जैसी mainstream GC general-purpose भाषाओं को देखें तो बात सही है। यह व्याख्या की जा सकती है कि object-oriented programming का मूल विचार आज के actor model के अधिक करीब था, जहाँ owned data structures को केवल message passing के ज़रिए बदला जाना था। लेकिन object-oriented के वास्तविक implementations उस लक्ष्य के करीब भी नहीं पहुँचे। Java एक ही object के mutable references को कई objects में रखने से नहीं रोकता। यह पोस्ट उस बात को बेहतर ढंग से खोलती है: https://without.boats/blog/references-are-like-jumps/
एक आसान क्विज़: यह code क्या print करेगा? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
संपादन: मैंने double negative को गलत पढ़ लिया। दोबारा पढ़ने पर भी अभी उलझन है। क्या इसका मतलब यह है कि Java में, JavaScript के विपरीत, local reasoning है?
मुझे आमतौर पर Graydon के लेख पसंद आते हैं, लेकिन यह लेख, formal methods पर कई लेखों की तरह, इस क्षेत्र से अपरिचित पाठकों को भ्रमित कर सकता है। यह कुछ वैसा है जैसे यह कहना कि सीसे को सोने में बदलने का तरीका एक अंक के पैमाने पर बेहतर हुआ है, लेकिन यह न कहना कि व्यावहारिक लागत-प्रभावशीलता तक पहुंचने के लिए अभी भी 29 अंकों के पैमाने की दूरी बाकी है
क्या no aliasing formal verification को बहुत आसान बनाता है? हाँ। लेकिन क्या इससे वास्तविक प्रोग्रामों को व्यावहारिक और लागत-प्रभावी तरीके से verify किया जा सकता है? बिल्कुल नहीं। हर दिन formally verified प्रोग्राम, circuits और components मौजूद हैं, लेकिन वे अपवाद के करीब हैं, तुलनात्मक रूप से बहुत छोटे हैं, और खास तौर पर बहुत सावधानी से बनाए जाते हैं। local reasoning में मदद करने वाले गुण महत्वपूर्ण हैं, लेकिन वे mainstream software की correctness को sound तरीके से guarantee करने के तरीकों में कोई वास्तविक बदलाव नहीं लाते
ऐसे language के प्रोग्राम भी, जिनमें heap नहीं, pointers नहीं, integers नहीं, सिर्फ boolean variables हों, और loops भी दो बार से ज्यादा न चल सकें—यानी जो Turing completeness से काफी दूर हों—TQBF में reduce हो जाते हैं, इसलिए उन्हें भी व्यावहारिक रूप से verify नहीं किया जा सकता। कुछ properties, जैसे memory safety, के लिए यह संभव हो सकता है, लेकिन software को जिन चीज़ों की ज़रूरत होती है उनके लिए यह पर्याप्त नहीं है। 1970–90 के दशक में यह आशा थी कि भले ही worst-case complexity संभालना कठिन हो, language की local guarantees और structure हमें worst case से बाहर रखेंगे, लेकिन बाद में यह गलत साबित हुआ। यह उम्मीद भी अब सही नहीं लगती कि लोग जो प्रोग्राम वास्तव में लिखते हैं, वे worst case से पर्याप्त दूर होते हैं ताकि अच्छे heuristics मिल सकें
इस विषय पर एक प्रस्तुति है: https://pron.github.io/posts/correctness-and-complexity
मुख्य परिणाम यह है कि जिन अधिकांश दिलचस्प properties को आप verify करना चाहते हैं, वे compositional नहीं होतीं। भले ही आप components P1...Pn में से हर एक के लिए property साबित कर दें, P1 ○ ... ○ Pn के लिए उस property को साबित करने की लागत सिर्फ n के लिए superpolynomial नहीं बढ़ती, बल्कि हर component के आकार के संदर्भ में भी superpolynomial बढ़ती है। यानी यह बिना विभाजन किए जितना कठिन है, लगभग उतना ही कठिन रहता है; correctness को हिस्सों में नहीं तोड़ा जा सकता। इसलिए “काफी कुछ verify किया जा सकता है” और “जो verify किया जा सकता है वह समुद्र में एक बूंद है” — दोनों बातें एक साथ सही हैं, और formal methods की चर्चाओं में यह खाई अक्सर गायब रहती है
पिछले 6 साल से अधिक समय से HN पर मैं यही तर्क सैकड़ों बार दोहरा चुका हूँ, और इस दौरान मिले बहुत से comments के बावजूद उसमें लगभग कोई नई बारीकी नहीं जुड़ी
यह पूरी तरह गलत नहीं है, लेकिन पूरी तरह सही भी नहीं। इस विषय में रुचि रखने वाले बहुत से लोगों को सैकड़ों दोहरावों के दौरान यह दिखाने का काफी अवसर मिला है, फिर भी उनकी स्थिति ज़रा भी विकसित नहीं हुई—यह आश्चर्यजनक है। ऐसा रवैया लगभग रोगग्रस्त बंद मानसिकता जैसा लगता है, और बातचीत में शामिल सभी लोगों का समय बर्बाद करता है
मेरा मानना है कि soundness पर फोकस करना, अधिक सही software के लक्ष्य में मदद करने के बजाय, वास्तव में उन techniques से ध्यान हटा देता है जिन्होंने व्यवहार में बेहतर परिणाम दिए हैं। ऐसी practical techniques मौजूद हैं जिन्हें theoretical support भी मिला हुआ है, और वे कभी-कभी उन लोगों को भी चौंका देती हैं जो soundness को ही एकमात्र रास्ता मानते थे: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
यह बार-बार होता है। जब sound methods में महत्वपूर्ण सुधार आते रहते हैं, तब भी unsound methods व्यवहार में अधिक सही software की दिशा में कहीं बड़ी प्रगति हासिल करते हैं। इसका एक बहुत हालिया उदाहरण https://antithesis.com है। बेशक, कुछ खास परिस्थितियों में sound techniques अधिक शक्तिशाली और व्यावहारिक हो सकती हैं, इसलिए यह एक जटिल विषय है
यह उम्मीद करना उचित है कि हम छोटे Rust libraries में unsafe के सही उपयोग को verify कर सकेंगे। केवल वही भी सचमुच बहुत उपयोगी होगा
मैंने अभी F* लेख पर भी इससे संबंधित comment किया है। syntax के मामले में मुझे व्यक्तिगत रूप से Rust की तुलना में F*/F# अधिक पसंद है, लेकिन विकसित किए जा रहे शो नियंत्रण software के लिए मैंने Ada/SPARK2014 चुनने का फैसला किया है
अगर Rust को Ada/SPARK2014 जैसे लोगों को आकर्षित करना है, तो उसे C, Common Lisp, Prolog, Fortran, COBOL जैसी पुरानी languages की तरह एक औपचारिक प्रकाशित standard चाहिए। AdaCore और Ferrous Systems, Ada/SPARK2014 की तरह Rust के लिए formal verification tools देने के लिए सहयोग करते हुए Rust को उस दिशा में ला रहे हैं, लेकिन अभी तक कोई प्रकाशित standard नहीं है, और Ada तथा SPARK2014 की विरासत बहुत बड़ी है
यह दिलचस्प है कि reference counting को एक तरह के तुरंत चलने वाले optimized GC के रूप में देखा जा सकता है, जो या तो तब काम करता है जब इसे सख्ती से acyclic data पर इस्तेमाल किया जाए, या जब cyclic leak स्वीकार्य हो। Python इस लेख में बताए गए reference counting + tracing के मिश्रित तरीके का उपयोग करता है, और मैंने ऐसे production deployment भी देखे हैं जहाँ tracing collector को हर N requests में सिर्फ एक बार चलाने के लिए मजबूर किया जाता है
Perl pure reference counting का उपयोग करता है, लेकिन उसमें weak references हैं, इसलिए cyclic structure में किस हिस्से की references बनाए रखनी हैं इस पर ध्यान देने की कीमत पर data को reference counting के नज़रिए से acyclic बनाया जा सकता है। Koka सैद्धांतिक रूप से reference counting का उपयोग करता है, लेकिन व्यवहार में इसे जितना संभव हो compile time तक ले जाने की कोशिश करता है, और अगर y = x + 1 में यह सुनिश्चित हो कि x की सिर्फ एक ही reference है और बाद में उसका उपयोग नहीं होगा, तो y के लिए वही storage reuse करके in-place mutation की जा सकती है
Nim ORC प्रदान करता है, जो automatic reference counting में Bacon+Rajan के Recycler algorithm का implementation जोड़ता है। यह algorithm reference counting आधारित systems में सिर्फ cycles collect करने के लिए बनाया गया है, इसलिए काफी तेज है। Rust पर लौटें तो इसका stop-the-world Recycler implementation यहाँ है: https://github.com/fitzgen/bacon-rajan-cc और इस fork में bacon-rajan-ccc crate के रूप में वितरित किया गया है: https://github.com/mbartlett21/bacon-rajan-cc। README के Alternative सेक्शन में इसी क्षेत्र के दूसरे experiments के links हैं। अगर Recycler paper ढूँढना मुश्किल हो तो मैंने उसकी प्रतियाँ https://trout.me.uk/gc/ के नीचे इकट्ठी की हैं, और अगर आपकी रुचि मिलती-जुलती है तो https://trout.me.uk/lisp/ के नीचे के papers भी पसंद आ सकते हैं
Firefox भी C++ DOM objects और JS के ज़रिए बनने वाले cycles को संभालने के लिए reference counting के साथ trial deletion आधारित cycle collector का उपयोग करता है। वास्तव में Graydon ने शुरुआती implementation किया था
प्रोग्राम की formal verification को लेकर मैं अधीर महसूस करता हूँ। यह प्रमाणित करना कि कोई program specification को सही तरह implement करता है, सैद्धांतिक रूप से दिलचस्प है, लेकिन व्यावहारिक उपयोगिता कम है
सही specification लिखना सही programming करने जितना ही कठिन है, इसलिए मुश्किल समस्या हल नहीं होती, बस इधर से उधर खिसक जाती है। formal methods के व्यावहारिक उपयोग हैं, लेकिन वे कम ही मिलते हैं
पूरी specification के मामले में यह सही है, लेकिन आम तौर पर वही असली लक्ष्य नहीं होता। आम तौर पर आप कुछ मुख्य properties साबित करना चाहते हैं। जैसे यह function हमेशा terminate करेगा, या वह function हमेशा sorted array लौटाएगा
एक बार ऐसा किया जा सके तो उसे precondition के रूप में enforce किया जा सकता है। उदाहरण के लिए, किसी function को array देने से पहले यह दिखाना पड़े कि वह array पहले से sorted है
यह 15 मई 2024 को लिखा गया था, और उसी दिन Rust 1.0 की 9वीं वर्षगांठ थी
मैंने linked Boats post पढ़ी और वह शानदार थी। यह देखकर आश्चर्य हुआ कि Hoare का 50 साल पुराना उद्धरण आज भी प्रासंगिक है और अभिव्यक्ति भी बेहद अच्छी है
काश compile time पर type guard जैसी चीज़ें किसी अधिक सरल तरीके से इस्तेमाल की जा सकतीं। जब trait bounds बहुत बढ़ जाते हैं तो type-level programs पढ़ना मुश्किल हो जाता है
उदाहरण के लिए Where <<::Output as G>::Output as H>::Output: HList + Z या type Output = <<::Output as G>::Output as H>::Output; जैसी चीज़ें। फिर इसमें Cons>>> जोड़ दीजिए, और TypeNum के U8 जैसे नंबर भी अपने आप में Cons>> nesting हैं, यह समझ आता है। इस क्षेत्र में प्रगति करना और मनचाहा verification हासिल करना संभव है, लेकिन error messages इंसानी developers के code लिखने के तरीके से काफ़ी अलग हो सकती हैं, और implementation भी बहुत पीड़ादायक होता है
developer experience इसलिए चौंकाती है क्योंकि यह “सिर्फ functions” नहीं है, बल्कि कुछ specific generics और associated types का combination है। मैं runtime-style checks का उपयोग करना चाहता था, लेकिन उन्हें compile time पर चलाना चाहता था, और ऐसा करने के लिए काफ़ी अलग code लिखना पड़ा। आखिरकार, type-level compile-time Rust को अधिक सरल, functional और पढ़ने योग्य बनाना शायद ऐसा रास्ता हो सकता है जिससे इस तरह की formal analysis projects maintainers और users दोनों को अच्छा अनुभव दें। संक्षेप में, मुझे comptime Rust चाहिए। और यह भी सोचता हूँ कि Pin<&mut Self> आधारित Future क्या अब पहले से ही स्थिर रूप ले चुका है। मैं async/await की दूसरी internal implementations के साथ प्रयोग करना चाहता हूँ, लेकिन शुरू कहाँ से करूँ यह पता नहीं है
1 टिप्पणियां
Hacker News टिप्पणियाँ
यह एक अच्छी पोस्ट है। मैंने पहले program verification किया है, और उस नज़रिए से Rust आधुनिक भाषाओं में formal techniques लागू करने के लिए सबसे उपयोगी भाषा लगती है।
Rust के rules ऐसे कई मामलों को हटा देते हैं जिन्हें formalize करना मुश्किल होता है। बची हुई बड़ी समस्या thread दृष्टिकोण और
Rc/borrow दृष्टिकोण से deadlock analysis की है, और ये दोनों कुछ हद तक समतुल्य हैं। अगर Rust में static deadlock analysis हो, तो safe dereference pointers भी संभव हो सकते हैं, और अगर यह साबित किया जा सके कि सभी borrow/upgrade calls विफल नहीं होंगे, तो ज़्यादातर reference counting हटाई जा सकती है। तब जहाँ संभव हो, interior mutability भी लगभग मुफ़्त में मिल जाएगी।theorem provers की बड़ी समस्या यह है कि उन्हें theorem prove करना पसंद करने वाले लोग बनाते हैं, इसलिए वे formalism में फँस जाते हैं और programmers तथा UI की समझ से उनका तालमेल बिगड़ जाता है। ज़्यादातर proof obligations को SAT solver से संभाला जा सकता है, लेकिन कठिन समस्याओं के लिए भारी tools चाहिए। Coq बहुत ज़्यादा manual है, और लेखक के हिसाब से ACL2 बहुत functional है। machine learning theorem provers को दिशा देने में मदद कर सकता है। proof खुद उससे कराना कठिन है, लेकिन control flow और data usage में मोटे तौर पर समान code से proof plan infer करना संभव लगता है
Firefox और Wireguard के crypto routines Rust में नहीं, बल्कि F* में—और अधिक सटीक रूप से F* में एम्बेड किए गए low-level DSL Low* में—लिखे गए थे, और वे पूरी तरह verified हैं।
https://project-everest.github.io/
https://mitls.org/
Rust जैसी किसी बाहरी भाषा के verification में ऐसे tools लागू करने की समस्या यह है कि proofs target language में नहीं लिखे जाते, इसलिए developers को दो भाषाएँ सीखनी पड़ती हैं। Creusot लिखने के अनुभव, Verus और Aeneas पर काम, और Why3 lab के अनुभव के आधार पर मैं सोचता रहा हूँ कि “verification-aware Rust” कैसा दिखेगा। अगर ऐसी भाषा शुरुआत से बनाई जाए, तो verification ease में यह Rust से भी चरणबद्ध रूप से बेहतर हो सकती है, खासकर proof के कठिन हिस्सों में इसका असर बड़ा हो सकता है
built-in features में जो चीज़ सबसे ज़्यादा खलती है, वह “मेरे proof पर quickcheck चला दो” जैसी सुविधा है। जब आपके पास code हो और आप किसी ऐसी property को prove करने की कोशिश कर रहे हों जो वास्तव में सही नहीं है, तो proof क्यों नहीं हो रहा यह समझते-समझते सिर पकड़ना पड़ सकता है। अगर proof के बीच में कोई बेमतलब state आ जाए, तो “यहाँ से counterexample generate करो” जैसा command counterexample दे दे, तो अच्छा होगा। proofs बहुत path-dependent होते हैं और आम तौर पर आसान नहीं होते, लेकिन ये tools महानता के बहुत करीब लगते हैं। code को prove करने की प्रक्रिया में यह संभावना भी शामिल होनी चाहिए कि उस code में bug हो सकता है
prover कोई गलत proof नहीं निकालेगा; वह सिर्फ valid proof निकालने में विफल होगा। ऐसे गुण वाले machine learning applications ज़्यादा नहीं हैं
वास्तव में Rust में locks और reference counting runtime constructs हैं।
ArcRust के RAII model को काफ़ी हद तक तोड़ देता है, इसलिए scoped threads को हटाना पड़ा, जिनमें scope खत्म होने से पहले destructor चलना चाहिए था। global reference counting में cycles और leaks की समस्या है, इसलिए यह फिर से एक global समस्या बन जाती है। इसे पूरी तरह हटाना मुश्किल होगा, लेकिन मेरा मानना है कि इसे arena-style scopes में सीमित करना बेहतर है। locks की जगह channel जैसे asymmetric data structures ज़रूरी लगते हैं। Go में channel को sender और receiver में बाँटा जाता है, और sender goroutine मेंdefer close(ch)लगाया जा सकता है; panic हो जाए तब भी बाकी thread खत्म होने पर इसका चलना सुनिश्चित होता है। ज़रूरी नहीं कि वह channel ही हो, लेकिन read-write / producer-consumer भूमिकाएँ अलग कर देने से reasoning बहुत आसान हो जाती है और formal analysis में भी मदद मिल सकती है।यह अच्छा लगा कि बात Hoare के लगभग 1973 के पेपर के उद्धरण से शुरू होकर अब दूसरी पोस्ट तक पहुँची है। मैंने पहले boat की पोस्ट के HN थ्रेड में एक लंबी टिप्पणी लिखी थी कि उस उद्धरण को Rust-केंद्रित नज़रिए की ओर झुकाना, boat की पृष्ठभूमि को देखते हुए समझ में आता है, लेकिन इससे Hoare की आलोचना का दायरा कृत्रिम रूप से संकरा हो जाता है
अब Grayson ने उसी संकरे हिस्से को शुरुआती बिंदु बनाकर Rust के कुछ दिलचस्प क्षेत्रों और design points पर चर्चा की है। मुझे अब भी लगता है कि मेरी टिप्पणी सही थी, लेकिन Grayson की पोस्ट से निकली चर्चा उस मूल पोस्ट के बारे में मेरी तकनीकी शिकायतों की भरपाई करने के लिए काफी थी
उसके बाद, साधारण testing से आगे बढ़ी unsound techniques आने लगीं, और मुझे लगता है कि unsound methods sound methods से आगे निकल गए
उन्होंने समस्या पहचान ली थी, और पीछे मुड़कर देखें तो type system के ज़रिए shared XOR mutability को enforce करने वाला हल बस एक छोटा-सा कदम लगता है। अगर तब समझ आ गया होता कि वही छोटा कदम असल समाधान है, तो 50 साल की भारी पीड़ा कम हो सकती थी
लेकिन उद्धरण खुद इस दृष्टिकोण को मज़बूत करता हुआ नहीं लगता। इसे यूँ भी देखा जा सकता है कि Hoare के references के semantic अस्तित्व पर अधिक सामान्य विलाप को लेकर उसे Rust के non-aliased mutable state model पर लागू करके समस्या को bypass करने की कोशिश की जा रही है। पर यह ज़्यादा से ज़्यादा बड़ी समस्या के एक संकरे हिस्से को ठीक कर, फिर यह कहने जैसा है कि पूरी समस्या गायब हो गई। जो हिस्से छोड़ दिए गए हैं, खासकर “Variables” खंड की शुरुआत और ALGOL 68 का उदाहरण, वे इस ओर कहीं अधिक मज़बूती से इशारा करते हैं कि Hoare केवल mutable state नहीं बल्कि reference नाम की semantic concept की ही आलोचना कर रहे थे। मैं मानता हूँ कि Rust समस्या के एक हिस्से को काबू में लाने की कोशिश है, लेकिन मैं नहीं मानता कि किसी भी भाषा ने इस समस्या को “ठीक” कर दिया है
मुझे समझ नहीं आता कि इस पोस्ट की इतनी प्रशंसा क्यों हो रही है। ऐसा लगता है जैसे program analysis के कई पूरे क्षेत्रों को एक ही पैराग्राफ़ में समेट दिया गया हो। मुझे Graydon पसंद हैं और मैं उनके दृष्टिकोण का सम्मान करता हूँ, लेकिन यह पैराग्राफ़ बहुत ज़्यादा simplification करता है
यह कहना कि GC वाली भाषाओं में मज़बूत local reasoning support नहीं होता, एक strawman है। Pony जैसी भाषाएँ रही हैं जो type system में regions रखती हैं और फिर भी GC इस्तेमाल करती हैं। इसके अलावा pointer analysis और escape analysis जैसे पूरे क्षेत्र हैं, जो uniqueness infer करते हैं और तय करते हैं कि क्या दो references aliases हो सकते हैं। Static typing का एक केंद्रीय तत्व भी यही है कि classes और fields जैसी तकनीकों से heap को ऐसे हिस्सों में बाँटा जाए जो एक-दूसरे के alias न हों। बात JavaScript की नहीं है; ऐसा दिखाना ठीक नहीं कि Java/C#/Scala और अनगिनत GC भाषाओं में mutable state पर local reasoning नहीं होता
classes और fields mutable state पर पूरी local reasoning नहीं देते। क्योंकि class/object A, class/object B की mutable state पर निर्भर हो सकता है। Java-शैली की class inheritance भी समय के साथ program के evolve होने पर अपने-आप और जटिलता जोड़ती है
बेशक counterexamples हैं, लेकिन अगर Java, C#, Python जैसी mainstream GC general-purpose भाषाओं को देखें तो बात सही है। यह व्याख्या की जा सकती है कि object-oriented programming का मूल विचार आज के actor model के अधिक करीब था, जहाँ owned data structures को केवल message passing के ज़रिए बदला जाना था। लेकिन object-oriented के वास्तविक implementations उस लक्ष्य के करीब भी नहीं पहुँचे। Java एक ही object के mutable references को कई objects में रखने से नहीं रोकता। यह पोस्ट उस बात को बेहतर ढंग से खोलती है: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }संपादन: मैंने double negative को गलत पढ़ लिया। दोबारा पढ़ने पर भी अभी उलझन है। क्या इसका मतलब यह है कि Java में, JavaScript के विपरीत, local reasoning है?
मुझे आमतौर पर Graydon के लेख पसंद आते हैं, लेकिन यह लेख, formal methods पर कई लेखों की तरह, इस क्षेत्र से अपरिचित पाठकों को भ्रमित कर सकता है। यह कुछ वैसा है जैसे यह कहना कि सीसे को सोने में बदलने का तरीका एक अंक के पैमाने पर बेहतर हुआ है, लेकिन यह न कहना कि व्यावहारिक लागत-प्रभावशीलता तक पहुंचने के लिए अभी भी 29 अंकों के पैमाने की दूरी बाकी है
क्या no aliasing formal verification को बहुत आसान बनाता है? हाँ। लेकिन क्या इससे वास्तविक प्रोग्रामों को व्यावहारिक और लागत-प्रभावी तरीके से verify किया जा सकता है? बिल्कुल नहीं। हर दिन formally verified प्रोग्राम, circuits और components मौजूद हैं, लेकिन वे अपवाद के करीब हैं, तुलनात्मक रूप से बहुत छोटे हैं, और खास तौर पर बहुत सावधानी से बनाए जाते हैं। local reasoning में मदद करने वाले गुण महत्वपूर्ण हैं, लेकिन वे mainstream software की correctness को sound तरीके से guarantee करने के तरीकों में कोई वास्तविक बदलाव नहीं लाते
ऐसे language के प्रोग्राम भी, जिनमें heap नहीं, pointers नहीं, integers नहीं, सिर्फ boolean variables हों, और loops भी दो बार से ज्यादा न चल सकें—यानी जो Turing completeness से काफी दूर हों—TQBF में reduce हो जाते हैं, इसलिए उन्हें भी व्यावहारिक रूप से verify नहीं किया जा सकता। कुछ properties, जैसे memory safety, के लिए यह संभव हो सकता है, लेकिन software को जिन चीज़ों की ज़रूरत होती है उनके लिए यह पर्याप्त नहीं है। 1970–90 के दशक में यह आशा थी कि भले ही worst-case complexity संभालना कठिन हो, language की local guarantees और structure हमें worst case से बाहर रखेंगे, लेकिन बाद में यह गलत साबित हुआ। यह उम्मीद भी अब सही नहीं लगती कि लोग जो प्रोग्राम वास्तव में लिखते हैं, वे worst case से पर्याप्त दूर होते हैं ताकि अच्छे heuristics मिल सकें
इस विषय पर एक प्रस्तुति है: https://pron.github.io/posts/correctness-and-complexity
मुख्य परिणाम यह है कि जिन अधिकांश दिलचस्प properties को आप verify करना चाहते हैं, वे compositional नहीं होतीं। भले ही आप components P1...Pn में से हर एक के लिए property साबित कर दें, P1 ○ ... ○ Pn के लिए उस property को साबित करने की लागत सिर्फ n के लिए superpolynomial नहीं बढ़ती, बल्कि हर component के आकार के संदर्भ में भी superpolynomial बढ़ती है। यानी यह बिना विभाजन किए जितना कठिन है, लगभग उतना ही कठिन रहता है; correctness को हिस्सों में नहीं तोड़ा जा सकता। इसलिए “काफी कुछ verify किया जा सकता है” और “जो verify किया जा सकता है वह समुद्र में एक बूंद है” — दोनों बातें एक साथ सही हैं, और formal methods की चर्चाओं में यह खाई अक्सर गायब रहती है
यह पूरी तरह गलत नहीं है, लेकिन पूरी तरह सही भी नहीं। इस विषय में रुचि रखने वाले बहुत से लोगों को सैकड़ों दोहरावों के दौरान यह दिखाने का काफी अवसर मिला है, फिर भी उनकी स्थिति ज़रा भी विकसित नहीं हुई—यह आश्चर्यजनक है। ऐसा रवैया लगभग रोगग्रस्त बंद मानसिकता जैसा लगता है, और बातचीत में शामिल सभी लोगों का समय बर्बाद करता है
यह बार-बार होता है। जब sound methods में महत्वपूर्ण सुधार आते रहते हैं, तब भी unsound methods व्यवहार में अधिक सही software की दिशा में कहीं बड़ी प्रगति हासिल करते हैं। इसका एक बहुत हालिया उदाहरण https://antithesis.com है। बेशक, कुछ खास परिस्थितियों में sound techniques अधिक शक्तिशाली और व्यावहारिक हो सकती हैं, इसलिए यह एक जटिल विषय है
unsafeके सही उपयोग को verify कर सकेंगे। केवल वही भी सचमुच बहुत उपयोगी होगामैंने अभी F* लेख पर भी इससे संबंधित comment किया है। syntax के मामले में मुझे व्यक्तिगत रूप से Rust की तुलना में F*/F# अधिक पसंद है, लेकिन विकसित किए जा रहे शो नियंत्रण software के लिए मैंने Ada/SPARK2014 चुनने का फैसला किया है
अगर Rust को Ada/SPARK2014 जैसे लोगों को आकर्षित करना है, तो उसे C, Common Lisp, Prolog, Fortran, COBOL जैसी पुरानी languages की तरह एक औपचारिक प्रकाशित standard चाहिए। AdaCore और Ferrous Systems, Ada/SPARK2014 की तरह Rust के लिए formal verification tools देने के लिए सहयोग करते हुए Rust को उस दिशा में ला रहे हैं, लेकिन अभी तक कोई प्रकाशित standard नहीं है, और Ada तथा SPARK2014 की विरासत बहुत बड़ी है
यह दिलचस्प है कि reference counting को एक तरह के तुरंत चलने वाले optimized GC के रूप में देखा जा सकता है, जो या तो तब काम करता है जब इसे सख्ती से acyclic data पर इस्तेमाल किया जाए, या जब cyclic leak स्वीकार्य हो। Python इस लेख में बताए गए reference counting + tracing के मिश्रित तरीके का उपयोग करता है, और मैंने ऐसे production deployment भी देखे हैं जहाँ tracing collector को हर N requests में सिर्फ एक बार चलाने के लिए मजबूर किया जाता है
Perl pure reference counting का उपयोग करता है, लेकिन उसमें weak references हैं, इसलिए cyclic structure में किस हिस्से की references बनाए रखनी हैं इस पर ध्यान देने की कीमत पर data को reference counting के नज़रिए से acyclic बनाया जा सकता है। Koka सैद्धांतिक रूप से reference counting का उपयोग करता है, लेकिन व्यवहार में इसे जितना संभव हो compile time तक ले जाने की कोशिश करता है, और अगर
y = x + 1में यह सुनिश्चित हो किxकी सिर्फ एक ही reference है और बाद में उसका उपयोग नहीं होगा, तोyके लिए वही storage reuse करके in-place mutation की जा सकती हैNim ORC प्रदान करता है, जो automatic reference counting में Bacon+Rajan के Recycler algorithm का implementation जोड़ता है। यह algorithm reference counting आधारित systems में सिर्फ cycles collect करने के लिए बनाया गया है, इसलिए काफी तेज है। Rust पर लौटें तो इसका stop-the-world Recycler implementation यहाँ है: https://github.com/fitzgen/bacon-rajan-cc और इस fork में bacon-rajan-ccc crate के रूप में वितरित किया गया है: https://github.com/mbartlett21/bacon-rajan-cc। README के Alternative सेक्शन में इसी क्षेत्र के दूसरे experiments के links हैं। अगर Recycler paper ढूँढना मुश्किल हो तो मैंने उसकी प्रतियाँ https://trout.me.uk/gc/ के नीचे इकट्ठी की हैं, और अगर आपकी रुचि मिलती-जुलती है तो https://trout.me.uk/lisp/ के नीचे के papers भी पसंद आ सकते हैं
प्रोग्राम की formal verification को लेकर मैं अधीर महसूस करता हूँ। यह प्रमाणित करना कि कोई program specification को सही तरह implement करता है, सैद्धांतिक रूप से दिलचस्प है, लेकिन व्यावहारिक उपयोगिता कम है
सही specification लिखना सही programming करने जितना ही कठिन है, इसलिए मुश्किल समस्या हल नहीं होती, बस इधर से उधर खिसक जाती है। formal methods के व्यावहारिक उपयोग हैं, लेकिन वे कम ही मिलते हैं
एक बार ऐसा किया जा सके तो उसे precondition के रूप में enforce किया जा सकता है। उदाहरण के लिए, किसी function को array देने से पहले यह दिखाना पड़े कि वह array पहले से sorted है
यह 15 मई 2024 को लिखा गया था, और उसी दिन Rust 1.0 की 9वीं वर्षगांठ थी
मैंने linked Boats post पढ़ी और वह शानदार थी। यह देखकर आश्चर्य हुआ कि Hoare का 50 साल पुराना उद्धरण आज भी प्रासंगिक है और अभिव्यक्ति भी बेहद अच्छी है
काश compile time पर type guard जैसी चीज़ें किसी अधिक सरल तरीके से इस्तेमाल की जा सकतीं। जब trait bounds बहुत बढ़ जाते हैं तो type-level programs पढ़ना मुश्किल हो जाता है
उदाहरण के लिए
Where <<::Output as G>::Output as H>::Output: HList + Zयाtype Output = <<::Output as G>::Output as H>::Output;जैसी चीज़ें। फिर इसमेंCons>>>जोड़ दीजिए, और TypeNum केU8जैसे नंबर भी अपने आप मेंCons>>nesting हैं, यह समझ आता है। इस क्षेत्र में प्रगति करना और मनचाहा verification हासिल करना संभव है, लेकिन error messages इंसानी developers के code लिखने के तरीके से काफ़ी अलग हो सकती हैं, और implementation भी बहुत पीड़ादायक होता हैdeveloper experience इसलिए चौंकाती है क्योंकि यह “सिर्फ functions” नहीं है, बल्कि कुछ specific generics और associated types का combination है। मैं runtime-style checks का उपयोग करना चाहता था, लेकिन उन्हें compile time पर चलाना चाहता था, और ऐसा करने के लिए काफ़ी अलग code लिखना पड़ा। आखिरकार, type-level compile-time Rust को अधिक सरल, functional और पढ़ने योग्य बनाना शायद ऐसा रास्ता हो सकता है जिससे इस तरह की formal analysis projects maintainers और users दोनों को अच्छा अनुभव दें। संक्षेप में, मुझे
comptimeRust चाहिए। और यह भी सोचता हूँ किPin<&mut Self>आधारितFutureक्या अब पहले से ही स्थिर रूप ले चुका है। मैंasync/awaitकी दूसरी internal implementations के साथ प्रयोग करना चाहता हूँ, लेकिन शुरू कहाँ से करूँ यह पता नहीं है