औपचारिक विधियाँ और प्रोग्रामिंग का भविष्य

 (blog.janestreet.com)
1 पॉइंट द्वारा GN⁺ 5 시간 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • औपचारिक विधियाँ ऐसे टूल हैं जो यह साबित करते हैं कि सॉफ़्टवेयर इच्छित गुणों को पूरा करता है, और agent coding के फैलाव से लागत-उपयोगिता का आकलन बदल रहा है
  • Jane Street पहले मानता था कि कुछ विशेष मामलों को छोड़कर औपचारिक विधियों का लागत के मुकाबले मूल्य कम है, लेकिन अब वह समर्पित टीम बना रहा है
  • seL4 में 8,700 पंक्तियों के C code के सत्यापन में 25 person-years लगे, और code की हर एक पंक्ति पर लगभग 23 पंक्तियों का proof और आधा person-day verification लगा
  • agents द्वारा बनाया गया code अभी release करने योग्य quality से अलग है, और verification bottleneck कम करने तथा agents को मज़बूत feedback देने के साधन के रूप में औपचारिक विधियाँ महत्वपूर्ण हो रही हैं
  • Jane Street का मानना है कि उसके पास language पर गहरा नियंत्रण है और तैयार programmer community भी है, इसलिए OxCaml और proof-oriented techniques को साथ में आगे बढ़ाने की गुंजाइश है

औपचारिक विधियाँ और प्रोग्रामिंग का भविष्य

  • Jane Street पिछले 25 वर्षों से कहता आया था कि संगठन स्तर पर उसे औपचारिक विधियों में रुचि नहीं है, लेकिन अब वह इस रुख पर कायम नहीं है
  • बेहतर code और अधिक भरोसेमंद code लिखने वाले टूल्स की शक्ति को वह लंबे समय से महत्व देता रहा है, और type system को बड़ा लाभ देने वाली हल्की औपचारिक विधि माना गया है
  • विशेष मामलों, खासकर hardware synthesis को छोड़कर, उसका आकलन था कि औपचारिक विधियों की लागत इतनी अधिक है कि वे अधिकांश सॉफ़्टवेयर के लिए उपयुक्त नहीं हैं
  • seL4 एक formally verified microkernel है और एक महत्वपूर्ण उपलब्धि भी, लेकिन 8,700 पंक्तियों के C code के सत्यापन में 25 person-years लगे
    • code की हर पंक्ति पर लगभग 23 पंक्तियों के proof की ज़रूरत पड़ी, और एक पंक्ति के verification में लगभग आधा person-day लगा
  • security-critical microkernel जैसे मामलों में, जहाँ जोखिम बड़ा हो और specification अपेक्षाकृत स्पष्ट हो, यह तरीका मूल्यवान हो सकता है
  • लेकिन यह अधिकांश सॉफ़्टवेयर के लिए उपयुक्त नहीं था, और Jane Street को लगा कि उसके सबसे महत्वपूर्ण सॉफ़्टवेयर के लिए भी यह फिट नहीं बैठता
  • agent coding के आने से यह आकलन बदल गया, और औपचारिक विधियों की संभावना को लेकर संदेह अब उम्मीद में बदल रहा है
  • Jane Street formal methods team बना रहा है, और उम्मीद करता है कि इसे sophisticated type systems जितना व्यापक रूप से उपयोगी software-building tool बनाया जा सके

सोच क्यों बदली

  • agent coding कई तरीकों से औपचारिक विधियों की पारंपरिक लागत-उपयोगिता संरचना को हिला देता है
  • इसका मतलब यह नहीं कि agents अपने आप मनमाने कठिन proof बना सकते हैं, लेकिन models बड़ी मदद देते हैं और अधिक लोगों को इन टूल्स का उत्पादक उपयोग करने लायक बनाते हैं
  • चूँकि औपचारिक विधियों का उपयोग पहले की तुलना में आसान हो रहा है, इसलिए पुराने cost-benefit आकलन पर फिर से विचार करना उचित है

  • verification bottleneck अब अधिक महत्वपूर्ण है

    • models उपयोगी code लिखने में लगातार बेहतर हो रहे हैं, लेकिन model-generated code और वास्तव में release किए जा सकने वाले code के बीच अब भी बड़ा अंतर है
    • models दिए गए लक्ष्य को हासिल करने में चौंकाने वाले रूप से अच्छे हैं, लेकिन उस प्रक्रिया में codebase की quality को बनाए रखने या सुधारने में अभी पर्याप्त मज़बूत नहीं हैं
    • agents द्वारा लिखा गया code बेहतर हो रहा है, लेकिन उसमें अक्सर ज़रूरत से ज़्यादा complexity, अजीब bugs, edge cases, और codebase के मुख्य invariants का पालन न करने की प्रवृत्ति होती है
    • इंसानों को यह verify करने में बहुत समय लगाना पड़ता है कि agents द्वारा लिखा code पर्याप्त quality का है या नहीं
    • औपचारिक विधियाँ इस verification burden को कम कर सकती हैं और review process को अधिक efficient बना सकती हैं

  • agents feedback से मज़बूत होते हैं

    • agents, चाहे reinforcement learning के दौरान प्रशिक्षित किए जा रहे हों या coding में उपयोग किए जा रहे हों, feedback से लाभ उठाते हैं
    • औपचारिक विधियाँ agents की कठिन समस्याएँ हल करने की क्षमता बढ़ाने वाला एक शक्तिशाली feedback form बन सकती हैं
    • testing भी बहुत मूल्यवान है, और property-based testing तथा fuzzing के उपयोग से इसे और बेहतर बनाया जा सकता है
    • लेकिन केवल testing पर्याप्त नहीं है, और program जिन state spaces को explore कर सकता है उन्हें cover करने में इसकी अंतर्निहित सीमाएँ हैं
    • OxCaml programming experience में agents को type system द्वारा मिलने वाली universal guarantees से बड़ा लाभ मिलता है
    • अगर type system data races को रोक सकता है, तो data races को हटाया जा सकता है
    • अगर types को इस तरह बनाया जाए कि cross-site scripting vulnerabilities असंभव हो जाएँ, तो साधारण testing से कठिन तरीके से vulnerabilities को हटाया जा सकता है
    • types, agents के साथ programming करते समय verification bottleneck को कम करते हैं और बेहतर feedback देते हैं
    • अधिक शक्तिशाली proof techniques का उपयोग करने से अतिरिक्त सुधार की गुंजाइश हो सकती है

यह काम यहीं क्यों

  • पूरी दुनिया इस पर विचार कर रही है कि agents का programming के भविष्य के लिए क्या मतलब है, और औपचारिक विधियों व agents को जोड़ने की कोशिश करने वाले कई startups भी हैं
  • Jane Street अपने उपयोग की language पर गहरा नियंत्रण रख सकता है, इसलिए language को proof-oriented techniques के लिए अधिक उपयुक्त बनाया जा सकता है
  • संभावित दिशाएँ कई हैं
    • properties की modular specifications को type system में integrate किया जा सकता है
    • ownership और mutability जैसी चीज़ों पर type-level constraints जोड़कर कुछ proofs को आसान बनाया जा सकता है
    • proof techniques को सीधे language में डाला जा सकता है

  • तैयार programmer community

    • Jane Street के पास ऐसी programmer community है जो इन techniques को अपनाने के लिए तैयार है
    • programming languages पर काम करने वालों के लिए, बेहतर programming ideas बनाना अक्सर उतना कठिन नहीं होता जितना उन्हें वास्तविक काम में इस्तेमाल करवाना
    • Jane Street में अक्सर users इस बात की शिकायत करते हैं कि वादे किए गए नए और अपरिचित type system features पर्याप्त तेज़ी से नहीं आ रहे
    • ऐसे techniques का उपयोग करने की पृष्ठभूमि वाले लोग यहाँ बहुत हैं, और सही परिणाम तथा high-quality software बनाने में रुचि भी पहले से मौजूद है
    • सक्रिय और ऊँची अपेक्षाओं वाला user base, short-term improvements और long-term vision दोनों को साथ लेकर चलने की आज़ादी देता है
    • short-term improvements अपेक्षाकृत जल्दी प्रभाव डाल सकते हैं
    • long-term vision कई वर्षों में हासिल होने वाला अधिक महत्वाकांक्षी लक्ष्य बन सकता है
    • short-term प्रयासों से सीखते हुए long-term goals की ओर बढ़ा जा सकता है

  • बाहरी टूल्स के साथ संबंध

    • बाहरी दुनिया में हो रहे काम को नज़रअंदाज़ नहीं किया जा रहा, और कई programming language communities के काम से उम्मीद और प्रेरणा मिल रही है
    • संबंधित टूल्स में Lean, Dafny, Rocq, Agda, Iris शामिल हैं
    • OxCaml को कुछ टूल्स के साथ integrate करके पहले से मौजूद बेहतरीन infrastructure का उपयोग करने के तरीके खोजे जा रहे हैं
    • साथ ही यह भी माना जा रहा है कि language और proof techniques को एक साथ संभालने पर ही कुछ विशिष्ट लाभ हासिल किए जा सकते हैं

जुड़ने का आमंत्रण

  • Jane Street London और New York में formal methods से जुड़ी भूमिकाओं के लिए लोगों की तलाश कर रहा है
  • फिलहाल इन पदों के interview और team-building शुरुआती चरण में हैं
  • आगे किया जाने वाला काम बहुत अधिक है, और team में शामिल होने वाले लोगों की तलाश जारी है

पूरक

  • complex proofs से निपटते समय models को अब भी इंसानी मदद और मार्गदर्शन की ज़रूरत होती है
  • human programmers के पास इस बात के ideas हो सकते हैं कि system क्यों काम करता है और उच्च स्तर पर उसे कैसे prove किया जाए
  • अधिकांश programmers यह नहीं जानते कि किसी विशेष proof system को संतुष्ट करने वाले तरीके से proof ideas को encode कैसे किया जाए
  • models proof लिखने के technical details में बहुत-सा दोहराव वाला काम automate कर सकते हैं और विशेषज्ञता दे सकते हैं
  • Obj.magic जैसे escape hatches type-level constraints को bypass करने दे सकते हैं
  • अधिकांश code में ऐसे exceptions को track और ban कर दिया जाए, तो universal guarantees के बहुत क़रीब पहुँचा जा सकता है
  • औपचारिक विधियाँ यह स्पष्ट रूप से व्यक्त कर सकती हैं कि ऐसे escape hatches का उपयोग वास्तव में सुरक्षित क्यों है

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

1 टिप्पणियां

 
GN⁺ 5 시간 전
Hacker News की राय

  • कई दशक पहले correctness proofs पर काम किया था, और उस समय के सिस्टमों में बाद के कई सिस्टमों की तुलना में ज़्यादा proof automation था
    आसान हिस्से सबसे पहले SAT solver, Oppen-Nelson simplifier, संभाल लेता था, और कठिन हिस्से Boyer-Moore prover करता था, जो heuristics और पहले के lemmas का उपयोग करता था। इंसानों का कठिन काम यह था कि prover क्या-क्या कोशिश करे और बाद की proofs में इस्तेमाल होने वाले lemmas कौन से हों, यह सुझाना
    बाद के सिस्टमों में automation कम हो गई लगती है, और मेरा मानना है कि formal methods के भटकने की वजह यह थी कि वे व्यावहारिक काम से ज़्यादा formalism में फँस गए। commercial projects में bug-free code चाहने वाले व्यक्ति के नज़रिये से, ऐसा लगा कि अकादमिक प्रोजेक्ट गणितज्ञों की उस पसंद की तरफ झुक गए जो papers के लिए संक्षिप्त notation और कम case analysis को तरजीह देती है
    वास्तविकता में बहुत सारा automated grunt work चाहिए होता है और insight कम चाहिए होनी चाहिए। चतुर लोग paper-and-pencil proofs की लंबाई से बचने के लिए modal logic, temporal logic जैसी नई logics बनाते रहे, लेकिन उससे ज़्यादा मदद नहीं मिली। इस क्षेत्र की बुनियादी सच्चाई यह है कि अधिकांश theorems काफ़ी साधारण होते हैं
    जैसा Jane Street के लोग कहते हैं, language को नियंत्रित कर पाना एक बड़ा फ़ायदा है। verification statements को programming language के भीतर integrate होना चाहिए; अगर वे comments, अलग syntax, या अलग files में बंद हों तो बेवजह का काम बढ़ता है। Jane Street का इस दिशा में ज़ोर लगाना अच्छा लगता है
    यह काम मैंने 40 साल से भी पहले बहुत जल्दी कर लिया था, और उस समय Boyer-Moore prover के साथ number theory को शुरुआत से खड़ा करने में लगभग 45 मिनट की compute time लगती थी, जबकि अब इसमें 1 सेकंड से भी कम लगता है
    https://archive.org/details/manualzilla-id-5928072/page/n3/m...

    • formal methods में लंबे समय से काम करने वाले के तौर पर, नई logics मददगार नहीं रहीं—इस बात से थोड़ा असहमत हूँ। industrial logics व्यावहारिक हैं, और वे सिस्टम द्वारा संतुष्ट की जाने वाली परिष्कृत properties को बहुत संक्षेप में लिखने देती हैं
      logic की स्थिति computer science और software engineering में कुछ वैसी ही है जैसी physics, mechanical engineering, और civil engineering में calculus की है। LTL और हाल की separation logic जैसी चीज़ें बहुत बड़े breakthroughs थीं
      काफ़ी लोकप्रिय हुई TLA+ इसका सबूत है, और model checking बेहद व्यावहारिक है। अभी दिलचस्प बात यह है कि क्या और भारी formal methods, खासकर theorem proving, इतने सस्ते हो सकते हैं कि सामान्य system software में भी उनका उपयोग किया जा सके
      functions के लिए formal specifications लिखकर, SAT/SMT, theorem provers, और LLM के hybrid से synthesis कराना और correctness prove कराना जल्द ही standard बन सकता है
      On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
      From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
    • formal specifications में इंसानों द्वारा समझा और लिखा जा सकना वाकई बहुत महत्वपूर्ण होगा
      चिंता यह है कि ऐसी गणित विकसित हो जाए जिसे समझना मुश्किल हो, और उसे बचाने वाला कुछ आस्थावानों का छोटा समूह बन जाए। अलग-अलग कठिन notations आपस में compatible नहीं होंगे, और एक समझ लेने पर भी दूसरी को समझने में बहुत मदद नहीं मिलेगी। ज़्यादातर लोग अंत में सिर्फ़ अंग्रेज़ी वाक्य ही लिखेंगे जिन्हें ठीक से verify नहीं किया जा सकता
      इससे भी बुरा यह हो सकता है कि लोग मशीन से अपने वाक्यों को formalize करवाएँ, फिर उस formalism या proof को समझे बिना verification theater में हिस्सा लेते रहें, और जब सब कुछ फट पड़े तो हैरान होने का नाटक करें
    • सोच रहा हूँ कि क्या आपने Ada/SPARK देखा है। अगर देखा है, तो क्या यह आपके उस intuition से मेल खाता है कि चीज़ें कैसे होनी चाहिए
      type system जिन हिस्सों को तेज़ी से handle नहीं कर सकता, उनमें इस तरह की क्षमताएँ integrate करने का काम धीरे-धीरे चल रहा है, इसलिए इस रास्ते पर पहले चल चुके लोगों का नज़रिया दिलचस्प है

  • बढ़िया। पिछले कुछ महीनों में मैं Scala 3 में expressive types का उपयोग करके types में compile-time proofs को धीरे-धीरे और ज़्यादा समाहित कर रहा हूँ। macros का उपयोग नहीं करता, हालाँकि कुछ उपयोगी हैं
    यह तरीका सिर्फ़ agentic testing के फैलने वाली समस्या को कम करने में मदद नहीं करता, बल्कि ऐसा लगता है कि यह agents को low-quality working style में गिरने से भी रोकता है। ख़ास तौर पर, जब agent को उचित रूप से generalize करना चाहिए तब भी हर चीज़ के लिए नया singleton type बनाने वाली noun accumulation को यह रोकता है
    मेरी नज़र में अच्छी quality की agent coding को तेज़ करने वाली दिशा formal methods जैसी tools की दिशा है, जिसमें strong type systems वाली languages भी शामिल हैं
    यहाँ expressive types से मतलब ऐसी techniques से है जिन्हें आप सामान्य codebase में नहीं डालना चाहेंगे, जब तक कि team पहले से type-level programming में सहज न हो। यानी ऐसी team हो जहाँ higher-kinded types और type functions अजीब चीज़ें नहीं बल्कि बुनियादी building blocks हों
    knowledge के मामले में agents ज़्यादातर developers से “math” में बेहतर हैं, और कई बार category theory में डूबे developers से भी बेहतर होते हैं। ऊपर से, बातचीत के लिए उनके पास मानो “अनंत” patience हो, इसलिए वे सिखाने में भी काफ़ी अच्छे हैं
    व्यक्तिगत रूप से, मैंने Codex से कुछ hobby proofs को Lean-style में बदलवाया था और यह बहुत आसान था। मैं यह नहीं कहूँगा कि यह 100% “correct” है, और ज़्यादा सख़्ती से जाँचने के लिए मुझे Lean 4 और सीखना होगा, लेकिन बुनियादी तौर पर यह क्लासिक proof pitfalls भी जाँचता हुआ लगता है। formal methods का भविष्य मुझे बहुत रोमांचक लग रहा है

  • ऐसा लगता है कि बात यह है कि Gen AI बहुत सारा code बना रहा है, इसलिए इंसानों की value को verification की तरफ शिफ्ट किया जाए। मैं कभी-कभी सोचता हूँ कि programming असल में है क्या।
    जिन लोगों की मातृभाषा अंग्रेज़ी नहीं है, उनके लिए programming सीखना अपने-आप में एक बड़ी चुनौती है। बिना अनुवाद वाले English docs को समझने के लिए machine translation पर निर्भर रहना पड़ता है, और मेरी भाषा में उपलब्ध सामग्री लगभग 5–6 साल पीछे रहती है।
    अब AI द्वारा बनाए गए दसियों हज़ार lines of code का code review करना नामुमकिन होता जा रहा है, इसलिए गणितीय proof जैसी absolute rules बनाने की चर्चा दिखती है। यह पढ़कर मुझे Rust का borrow checker याद आया। सच में Rust को कुछ बार इस्तेमाल करो तो लोग borrow checker से बचने के लिए जुगाड़ू shortcuts अपनाने लगते हैं, और यह एक बुरी आदत बन जाती है।
    जब गणितीय सख्ती बहुत ज़्यादा हो जाती है, तो इंसान bypass ढूँढने लगता है। मेरे जैसे कम औपचारिक शिक्षा वाले programmers के लिए यह और भी आसान है।
    लगता है कि ऐसी कोशिशें आखिरकार सिर्फ़ कुछ खास formalized answers के लिए code लिखवाएँगी। अगर सब इतना standardized हो गया, तो क्या वह इंसानी ज़रूरतों का जवाब दे पाएगा, इस पर मुझे यक़ीन नहीं है।
    ऐसी defensive programming की कोशिशें ठीक हैं, लेकिन मेरी अपनी भाषा में कहूँ तो मैं aggressive programming करना चाहता हूँ। यानी risk लो, लेकिन जल्दी fix करो और deploy करो, और भरोसा रखो कि समय के साथ चीज़ें काफ़ी अच्छी हो जाएँगी।
    बेशक Jane Street जैसी जगहों पर, जहाँ accuracy बहुत महत्वपूर्ण है और काम का दायरा साफ़-साफ़ defined है, इस लेख का approach सही बैठता है। क्योंकि वहाँ market की demands को ठीक से model करने लायक data काफ़ी है।
    लेकिन मेरे जैसे, जो पैसा कमाने के लिए सोने की खान खोजते हुए लगातार जगह बदलते रहते हैं, ऐसे सामाजिक रूप से असफल इंसान के लिए यह methodology एक luxury जैसी लगती है। mature modeling वाले मौजूदा business को highly educated specialists द्वारा लगातार optimize किया जाना चाहिए, और मुझे पता है कि व्यवहारिक रूप से उस demand का पीछा कर पाना मुमकिन नहीं है। इसलिए मैं ऐसी जगहें ढूँढता हूँ जहाँ modeling structured न हो, लेकिन वहाँ भी यह approach काम आएगी या नहीं, पता नहीं।

    • इसे Jane Street के नज़रिए से देखना चाहिए। वे एक high-frequency trading company हैं और stocks तथा financial instruments को लाखों, शायद करोड़ों की units में trade करते हैं।
      वहाँ “बाद में ठीक कर लेंगे” जैसी कोई गुंजाइश नहीं होती। जब तक आप समझते हैं कि क्या गड़बड़ हुआ, तब तक शायद अरबों का नुकसान हो चुका हो।
      इसलिए aggressive तरीका non-core areas में चल सकता है।
      वैसे भी defensive approaches पहले से ही कई जगह इस्तेमाल हो रहे हैं। Python, Java वगैरह में garbage collector होता है, और एक अर्थ में यह verify करता है कि code इरादे के मुताबिक चले।
      मैं सोच रहा था कि formal verification कब से दिखना शुरू होगा, लेकिन implementation details की चिंता करने वाले चरण से समस्या को scientific और mathematical तरीके से describe करने वाले चरण तक जाना स्वाभाविक है।
    • aggressive programming जैसा expression मुझे अच्छा लगा। लेकिन वह paradigm तो पहले से ही industry की default state है।
      Gen AI की वजह से defensive programming की cost बहुत नीचे आ गई है, और human verification की cost बहुत ऊपर चली गई है। दूसरी तरफ formal methods verification को सस्ता बनाते हैं, लेकिन specification, types, proofs लिखने और implementation को एक कठोर ढाँचे में मोड़ने जैसी overhead बहुत बड़ी होती है।
      लेकिन Gen AI उस मुश्किल काम को automate कर सकता है। दोनों एकदम natural fit हैं।
    • अगर आप बिना अनुवाद वाले English docs के लिए machine translation पर निर्भर हैं, तो विषय से थोड़ा हटकर सही, लेकिन मैं English सीखने की ज़ोरदार सलाह दूँगा।
      थोड़ा effort लगेगा, लेकिन लगातार लगने वाला translation overhead हट जाए तो बहुत बड़ा फ़ायदा होगा।
    • मैं इस बात से सहमत हूँ कि ऐसी methodology एक luxury है। लेख में भी यह माना गया है, और Jane Street इस approach से फ़ायदा उठाने के लिए काफ़ी विशेष रूप से तैयार किया गया संगठन है।
    • Jane Street ने अपने लिए प्रासंगिक होने के कारण ऐसा लेख लिखा, यह स्वाभाविक है, और यह भी स्वाभाविक है कि यह हर तरह की programming पर सामान्य रूप से लागू नहीं होता।
      लेकिन कोई ख़ुद को “सामाजिक रूप से असफल” कहे या यह कहे कि अपने career में वह ऐसी practices का पालन नहीं करता, इसका इस तर्क से क्या संबंध है, यह मुझे ठीक से समझ नहीं आता।

  • मैं हाल ही में कुछ संबंधित ideas के साथ प्रयोग कर रहा हूँ, और जो बात चौंकाने वाली लगी वह यह थी कि frontier models, खासकर ChatGPT-5.5, Roqc, यानी पुराने Coq proof assistant में कुछ खास manual proofs को पूरा करने में कितने अच्छे हैं।
    proofs हमेशा सुंदर नहीं होते, लेकिन ChatGPT अक्सर कुछ ही मिनटों में, 10–100 iterations के भीतर, वह काम कर देता है जिसमें मुझे — जिसके पास proof assistants का सीमित लेकिन शून्य से अधिक अनुभव है और जिन lemmas को prove किया जा रहा है उस क्षेत्र का काफ़ी बड़ा domain experience है — बहुत ज़्यादा समय लगता।
    इस छोटे लेख के संदर्भ में यह दिलचस्प इसलिए है क्योंकि यह उन बुनियादी assumptions को हिलाता है जिन पर कुछ formal methods tools काम करते हैं। Frama-C, Ada/SPARK वगैरह इस बात पर केंद्रित हैं कि CVC5, Z3 जैसे tools अपने-आप discharge कर सकें ऐसे proof obligations generate किए जाएँ, और अगर वे fail हो जाएँ तो Roqc में manual proof वाले काफ़ी painful fallback पर जाना पड़ता है।
    आम flow यह होता है कि पहले पता चलता है कि कोई obligation “hard” है, यानी उसे automatically discharge नहीं किया जा सकता, फिर code में उस obligation के generation point पर दिखने वाले lemmas और assertions के सेट को फिर से गढ़ा जाता है ताकि वह “easy” बन जाए, या कभी-कभी code ही बदल दिया जाता है।
    यह उस दुनिया में समझ में आता है जहाँ Roqc proofs की cost दोगुनी मानी जाती है। इंसानों के लिए उन्हें लिखना कठिन है, और जब code तथा उसके आसपास के proofs बदलते हैं तो maintenance volatility भी बहुत ज़्यादा होती है।
    लेकिन अगर Roqc proof “AI के loop में auto-discharge” बन जाए, तो यह cost gap गायब हो जाता है। तब proofs को code की तरह लिखा जा सकेगा, जहाँ इंसानों के लिए readable clarity पहली प्राथमिकता होगी और compiler या prover optimization बहुत बाद में आएगा। इसके implications को मैं अभी पूरी तरह पचा नहीं पाया हूँ, लेकिन यह काफ़ी दिलचस्प है।

    • जब requirements बदल जाएँ और चीज़ prove ही न की जा सके, तब AI के proof को आसान बनाने के लिए code और requirements दोनों बदल देने की कितनी संभावना है?
      मैंने proofs के साथ काम नहीं किया है, लेकिन मैंने कभी-कभी यह ज़रूर देखा है कि अगर आप कहें “change के बाद यह test fail हो गया”, तो AI उस code को इस तरह ठीक करने के बजाय कि पुराना test और नया test दोनों pass हों, test को ही बदल देता है।
    • मेरा अनुभव भी कुछ ऐसा ही है, बस मैंने Lean चुना। वह उन features से ज़्यादा जुड़ा था जिन्हें मैं बनाना चाहता था।
      आगे क्या होगा, इसे लेकर उत्साहित हूँ।
    • जब आप कहते हैं कि ChatGPT कुछ मिनटों और 10–100 iterations में Roqc proofs कर देता है, तो यह कैसे पता चलता है कि proof खुद सही है?

  • जब भी मैं formal specification की बात पढ़ता हूँ, यह मुझे अक्सर “उसी test को बस किसी और तरीके से लिखना” जैसा लगता है, और उससे भी बुरा, “उसी implementation को किसी और तरीके से लिखना” जैसा
    दो बार लिखने से bug पकड़ने में मदद मिल सकती है, लेकिन अगर formal specification में भी test या implementation जैसे ही bug हो सकते हैं, तो इसमें ख़ास क्या है, यह मुझे ठीक से समझ नहीं आता
    मूल समस्या यह लगती है कि किसी program के कुछ करने को औपचारिक रूप से साबित करने के लिए उस “कुछ” को बहुत ठोस रूप से परिभाषित करना पड़ता है। तब यह असल में test या implementation को फिर से लिखने जैसा हो जाता है
    मैं कई सालों से इस विषय को बीच-बीच में देखता रहा हूँ, और हमेशा लगता है कि मैं कुछ miss कर रहा हूँ, लेकिन समझ नहीं आता कि क्या। क्या कोई समझा सकता है?

    • Dijkstra के मशहूर कथन की तरह, “program testing bugs की मौजूदगी दिखा सकती है, लेकिन उनकी अनुपस्थिति नहीं”
      testing की कमी यह है कि आप केवल वही behavior test कर सकते हैं जिनके problematic होने की आपने कल्पना की हो। जिन behavior के गलत हो सकने का आपको पता ही नहीं था, उन्हें पहले से ठीक करने के लिए toolbox में कुछ अधिक अनोखे tools चाहिए होते हैं। fuzz testing उस दिशा की एक शुरुआत है, और formal verification दूसरी
      बेशक, ऐसे tools की quality इस बात पर निर्भर करती है कि आप ऐसा व्यापक formal model कितनी अच्छी तरह लिखते हैं जो वांछित behavior को अनुमति दे और अवांछित behavior को रोके, और कई क्षेत्रों में हम अब भी हैरानी की हद तक उस बिंदु से दूर हैं
    • बड़ा अंतर यह है कि formal methods आपको हर चीज़ के लिए universal quantifier इस्तेमाल करने देते हैं
      उदाहरण के लिए, unit test में आप लिख सकते हैं कि “foo('abc') trailing whitespace के बिना string लौटाता है”
      लेकिन formal methods से आप यह साबित कर सकते हैं कि “किसी भी input x के लिए foo(x) trailing whitespace के बिना string लौटाता है”
      यह एक मामूली उदाहरण है, लेकिन आप इससे अधिक जटिल बात भी सोच सकते हैं, जैसे “किसी भी program P के लिए compile(P), P जैसा ही behavior करता है”
      बेशक, “वैसा ही behavior” क्या है, यह परिभाषित करना पड़ेगा
    • मैं software में इसका उपयोग नहीं करता, लेकिन ASIC और FPGA design में formal-method specification की मदद से SAT solver जैसे tools यह तय कर सकते हैं कि target design specification को satisfy करता है या नहीं
      आप design की properties बताते हैं, और tool design को कई तरीकों से जाँचकर देखता है कि क्या वह उन properties का उल्लंघन कर सकता है
      उदाहरण के लिए, अगर कोई system traffic signal control करता है, तो आप यह property दे सकते हैं कि एक-दूसरे को काटने वाली lanes एक ही समय पर, या एक निश्चित समय अंतराल के भीतर, दोनों हरी नहीं हो सकतीं
      tool इसे exhaustive search से जाँच सकता है और उल्लंघन करने वाला code trace दिखा सकता है
    • यह सिर्फ “उसी test को किसी और तरीके से लिखना” नहीं है। हर test आम तौर पर या तो स्वतंत्र होता है, या फिर इतना बड़ा हो जाता है कि संभालना मुश्किल हो जाए, और test suite की completeness का आकलन branch coverage जैसी अपेक्षाकृत मोटी overlap techniques से करना पड़ता है
      statically proven type system यह सुनिश्चित कर सकता है कि हर component को पहले से बाकी सभी components के साथ match करके जाँचा जाए। बात सिर्फ “यह test pass करता है” की नहीं है, बल्कि combine करने पर “ये सारे test मिलकर एक तर्कसंगत और consistent whole बनाते हैं” की गारंटी की है, और inconsistent model को code में implement होने से रोकने की है
      यह कुछ-कुछ Rust के match की उस शर्त को पूरे codebase के पैमाने पर बढ़ाने जैसा है, जिसमें हर possible branch को पूरी तरह cover करना ज़रूरी होता है
      यह सही है कि अगर आप logic या theory में मूलभूत गलती कर दें तो यह उसे नहीं पकड़ेगा। लेकिन फिर भी, उदाहरण के लिए Haskell type system, ad hoc functional testing, और property testing को जोड़ने से यह कहीं अधिक मज़बूत हो सकता है। वह भी कुल मिलाकर एक सशक्त व्यवस्था है, लेकिन formally proven cryptography का मानक उससे कहीं ऊँचा है
    • असली ताकत किसी खास test और पूर्ण प्रमाण के बीच के फ़र्क में है। अगर आप boundary condition test के बारे में सोच ही न पाएँ, तो वह छूट जाएगी। अगर model अच्छा हो, तो आप production में जाने से पहले उसके अस्तित्व को जानकर उसे ठीक कर सकते हैं
      यह खास तौर पर concurrency, distributed, और multithreaded स्थितियों में बहुत मूल्यवान है। race condition और deadlock को test करना और उनके बारे में तर्क करना बेहद कठिन है; जैसे सवाल कि “क्या A, B, C घटनाएँ A, C, B क्रम में हो सकती हैं?”
      मुझे लगता है कि इस क्षेत्र की परिपक्वता लगभग इस तरह आगे बढ़ेगी। पहला, LLM शुरुआत में भले ही “दूसरी बार करके देखना” जैसी post-hoc verification तक सीमित रहें, फिर भी वे formal methods को सीखने और इस्तेमाल करने की रफ़्तार बहुत बढ़ाएँगे
      दूसरा, यह automation की तरफ़ बढ़ेगा जहाँ LLM जाँचेंगे कि “implementation code बदल गया है; क्या इससे model टूटता हुआ दिख रहा है?”। यह तब भी निर्णायक नहीं होगा, लेकिन उस चीज़ की human review से तो बहुत बेहतर हो सकता है जो केवल कभी-कभार बदलती है
      तीसरा, असली छलांग उन tools को अगले स्तर पर ले जाने में होगी जो कहते हैं, “बस formal specification लिखो और implementation generate करो।” ऐसे code generation project पहले से कई हैं, लेकिन ज़्यादातर अभी उस स्तर तक पूरी तरह परिपक्व नहीं हुए हैं जो कंपनियाँ चाहती हैं। अगर LLM tools उनमें से किसी एक को आपकी ज़रूरत के मुताबिक ढालने में लगने वाले 1–2 साल के manual work को तेज़ कर सकें, तो क्या होगा

  • Kleppmann की पिछली पोस्ट https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... भी देखने लायक है, और जो चीज़ें type system या linter में डाली जा सकती हैं, उनके लिए तो जाहिर है वैसा करने पर विचार करना चाहिए
    उम्मीद है कि इसे लिखने के ज़्यादा आसान तरीके आएँगे। पोस्ट में आए tools में dafny और iris शायद industrial use के सबसे क़रीब लगते हैं। मुझे यह भी पता है कि Amazon S3 के अंदरूनी काम में TLA का इस्तेमाल होने का इतिहास रहा है
    लेकिन मुझे अभी तक इस क्षेत्र का TypeScript जैसा कुछ नहीं दिखा — ऐसा कुछ जो मौजूदा tools में स्वाभाविक रूप से फिट हो जाए, zero-cost abstraction की तरह काम करे, और जिसे लोग सच में पुराने तरीकों से ज़्यादा पसंद करें
    custom linter इस्तेमाल करना भी अभी काफ़ी खराब अनुभव है। golangci-lint एक पीड़ादायक codebase है, semgrep मैंने नहीं आज़माया, लेकिन उसका rule engine डराने वाला लगा। अभी तक मुझे कोई पसंद आने वाली AST API भी नहीं मिली

  • निगमनात्मक तर्क, यानी “formal methods”, की ऐसी प्रशंसा अक्सर इसकी बुनियादी सीमा को छोड़ देती है। सवाल यह है कि axioms और definitions target domain पर कितनी अच्छी तरह फिट बैठते हैं
    यह कुछ वैसा ही है जैसे कहना, “सिद्धांत में सिद्धांत और व्यवहार में कोई अंतर नहीं होता। व्यवहार में…”। मेरा अनुमान है कि Jane Street एक बड़ा codebase बनाए रखेगी जहाँ mapping 1:1 हो, क्योंकि कोड का उद्देश्य deterministic algorithms को implement करना है। बहुत से developers ऐसे domains में काम करते हैं, लेकिन लाखों लोग नहीं करते। ज़्यादातर UI, ज़्यादातर exploratory work, आदि ऐसे ही हैं
    formal methods के साथ-साथ एक और धारा भी है जो logical या mathematical तरीके से नहीं, बल्कि approval criteria को बहुत high resolution पर define करने की कोशिश करती है। यह धारा कम-से-कम mapping problem से जूझती है, लेकिन जहाँ-जहाँ नक्शा ज़मीन नहीं है, वहाँ ज़्यादातर जगह इसे हल नहीं कर पाती
    Google search results page के पास बेहद विकसित internal optimization framework है, लेकिन क्या वह सचमुच optimum तक पहुँचा है? क्या किसी धुंधले आइडिया को पकड़ने के लिए जल्दी में बनाया गया prototype बेहतर दिखा सकता था? ऐसे सवालों का सबसे अच्छा जवाब सिस्टम के अंदर नहीं, बल्कि उस बाहरी दुनिया को देखकर मिलता है जिसकी सेवा वह सिस्टम करता है

    • formal methods ठीक-ठीक उन domains के लिए हैं जिनकी semantics अच्छी तरह defined हो
      logic circuits, बहुत formal verification वाले CPU components, kernels, protocols, parsers, compilers, cryptography, security frameworks, concurrency primitives आदि verification से बहुत लाभ पाते हैं
    • असल में ज़्यादातर UI आखिरकार state machines पर आकर टिकते हैं, और यह formal verification के लिए बहुत अच्छी तरह उपयुक्त है
      और जानने के लिए Hillel Wayne की यह पोस्ट अच्छी शुरुआत है: https://www.hillelwayne.com/formally-specifying-uis/
    • Google results page खुद अच्छी तरह defined नहीं है, लेकिन उसके नीचे का शायद 90% से ज़्यादा code अच्छी तरह defined होगा
      और कुछ मामलों में, result अच्छी तरह defined न भी हो तो भी उससे सीखा जा सकता है, इसलिए यह सिर्फ बैठकर यह सोचने का मामला नहीं है कि क्या समझदारी होगी

  • programming languages के design और implementation में थोड़ी दिलचस्पी रखने वाले के नाते, यह वाक्य मुझे सचमुच दिलचस्प लगा। “Programming languages से जुड़े ज़्यादातर लोगों के लिए आसान हिस्सा यह है कि वे programming को बेहतर बनाने के लिए नए और बेहतर ideas निकाल लें। कठिन हिस्सा यह है कि किसी को मनाया जाए कि वह उन ideas को अपने असली काम में इस्तेमाल करे”
    पूरी तरह सहमत। फ़ायदा हो तब भी, किसी नई language में डाली जा सकने वाली अपरिचितता की मात्रा की एक सीमा होती है
    लेकिन AI agents शायद programming language design के radically new ideas के प्रति इतना प्रतिरोध महसूस नहीं करेंगे। मैं कुछ समय से सोच रहा हूँ कि agentic AI के बाद programming language design कैसे evolve करेगा
    जब adoption की चिंता बहुत कम रह जाए, तब यह देखना बहुत रोचक होगा कि programming languages को बेहतर बनाने के लिए कौन-से नए ideas बनाए जा सकते हैं
    https://steveklabnik.com/writing/the-language-strangeness-bu...

  • application security testing में formal methods लागू करने की दिशा में काम चल रहा है, और मेरा मानना है कि यही approach business logic verification पर भी लागू की जा सकती है
    इसके लिए taint analysis का इस्तेमाल किया जा रहा है। यह formal methods की काफ़ी अच्छी तरह स्थापित approach है, लेकिन real codebases में data flow की जटिलता के कारण इसे अभी तक field में व्यापक रूप से लागू नहीं किया गया है
    formal methods को AST pattern matching और साधारण type checking से आगे बढ़ाना वास्तव में बहुत कठिन काम है। taint analysis के ज़रिए real codebases में interprocedural data flow को कुछ ही मिनटों में trace करने और गहराई में छिपी vulnerabilities खोजने के स्तर तक पहुँचने में कई वर्षों का R&D लगा
    दिलचस्पी हो तो project देख सकते हैं: https://github.com/seqra/opentaint

  • लगभग 18 महीने पहले मैं LLM के साथ types इस्तेमाल करने का दीवाना हो गया था, और lean4 को मैंने लगभग 6–8 महीने पहले गंभीरता से लेना शुरू किया। अब मैं practical C/C++ FFI, और इसलिए लगभग हर चीज़ से जुड़ सकने वाले, CIC proof base के बिना software work में AI assistance इस्तेमाल करने पर विचार भी नहीं करता
    JSON से लेकर Python तक सब पर रोक लगा दी, और nix को भी इस तरह दोबारा लिखा कि उसमें compiler हो। हम जो लगभग सब कुछ इस्तेमाल करते हैं, वह सिर्फ property testing और कई fuzz tests से उसकी सीमा तक नहीं गुज़रता, बल्कि कम-से-कम .olean linkage के ज़रिए property tests चलाने वाला lean4 proof भी रखता है। समय मिले तो पूरे domain की completeness तक prove करते हैं और उस property का भी test करते हैं
    सारे fast parts lean4 से generate होते हैं, इसलिए C++/Rust बहस को छोड़ देते हैं। इसका फ़ायदा तब है जब C++ में bug दरअसल lean4 code का bug निकले, हालाँकि बात दोनों दिशाओं में जा सकती है
    यह बड़ा बदलाव है, और “JSON और Python पर रोक?” कहकर संदेह करने वालों को मैं दोष नहीं देता। लेकिन हमने इस तरीके से लाखों lines की जाँच की है, और AI + formal system की छलांग, AI न होने से AI और Python तक जाने की तुलना में कहीं बड़ी है। हमारे अनुभव में दूसरा रास्ता monotonic progress नहीं देता, जबकि पहला लगभग हमेशा monotonic रूप से आगे बढ़ता है
    काफ़ी दुस्साहसी काम भी संभव हैं। यह ISL और CuTe जैसी चीज़ों द्वारा model किए जाने वाले polyhedral tensor computation का formal proof है, और इसके ज़रिए C++23 के mdspan से device पर swizzling और tiling किया जा सकता है और यह भी prove किया जा सकता है कि वह सही है। हालांकि यह उदाहरण coverage के बारे में L'Hopital-शैली की दलील को अच्छी तरह नहीं दिखाता: https://github.com/b7r6/mdspan-cute
    नतीजा सचमुच बहुत तेज़ है, और पहली कोशिश से ही तेज़ है
    https://straylight.software/assets/lambda-hierarchy.svg

    • Agda और Idris 2 को CIC के नीचे रखना lambda hierarchy को, सबसे अच्छे हाल में भी, भ्रामक बना देता है
    • इसलिए जिज्ञासा है कि आपने कौन-सा software बनाया, और वह उपयोगी क्यों है