दिमाग में छोटे-छोटे प्रमाण बनाते हुए बेहतर प्रोग्रामर कैसे बनें

• बेहतर प्रोग्रामर बनने के लिए कोड लिखते समय दिमाग में छोटे-छोटे प्रमाण बनाने की आदत महत्वपूर्ण है
• Monotonicity, immutability, pre-conditions·post-conditions, और invariants जैसे विचार ऐसे mini-proof करने में मुख्य अवधारणाएँ हैं
• कोड बदलाव का पूरे सिस्टम पर पड़ने वाला असर (isolation, firewall) ध्यान में रखकर डिज़ाइन करना complexity और risk कम करने में बहुत मददगार है
• Induction का उपयोग करने पर recursive functions या structures की correctness को चरण-दर-चरण साबित किया जा सकता है
• ऐसी सोच अभ्यास और आदत से विकसित होती है, और वास्तविक mathematical proofs तथा algorithm problems का अभ्यास इसमें बहुत मदद करता है

---

परिचय और मुख्य विचार

• लेखक ने अनुभव बढ़ने के साथ कोड की correctness और speed बेहतर करने के लिए स्वाभाविक रूप से ‘दिमाग में छोटे प्रमाण बनाने की आदत’ विकसित की
• कोडिंग के दौरान अपेक्षित behavior को दिमाग में verify और reason करने की प्रक्रिया अभ्यास मांगती है, लेकिन इसमें निपुण होने पर कोड की गुणवत्ता स्पष्ट रूप से बेहतर हो जाती है
• इसे ठीक-ठीक कैसे करना है, यह सबसे महत्वपूर्ण नहीं है; अलग-अलग तरीकों से अपने लिए उपयुक्त अभ्यास किया जा सकता है

एकदिशता (Monotonicity)

• Monotonicity का मतलब है कि function या code केवल एक दिशा में आगे बढ़ता है
• उदाहरण के तौर पर checkpointing को लिया जा सकता है, जहाँ काम के चरण केवल आगे बढ़ते हैं और जो काम पूरा हो चुका है उसे पीछे जाकर दोबारा नहीं चलाया जाता
• LSM tree और B-tree की तुलना में, LSM tree में ज़्यादातर space जमा होती जाती है और केवल compaction प्रक्रिया में कम होती है
• अगर monotonicity सुनिश्चित हो, तो complex state या कुछ परिणामों को स्वाभाविक रूप से बाहर किया जा सकता है या पहले से अनुमानित किया जा सकता है
• Immutability भी इससे मिलता-जुलता विचार है; एक बार सेट किया गया value कभी नहीं बदलता, इसलिए state change की संभावनाएँ हट जाती हैं

पूर्व-शर्तें और परिणाम-शर्तें (Pre- and post-conditions)

• Pre-condition और post-condition वे दावे हैं जो किसी function ke चलने से पहले और बाद में अनिवार्य रूप से true होने चाहिए
• function लिखते समय इन conditions को स्पष्ट रूप से track करना logical thinking और testing दोनों में मदद करता है
• post-condition को स्पष्ट रूप से तय करने पर unit test cases निकालना आसान हो जाता है
• कोड में इन conditions को जाँचने वाले assertion जोड़कर unexpected situations में जल्दी रुकना predictability और safety बढ़ाता है
• कई बार किसी function के लिए साफ pre/post-conditions देना ही कठिन होता है; इसे पहचान लेना भी अपने-आप में महत्वपूर्ण संकेत है

अपरिवर्तनीय शर्तें (Invariants)

• Invariant वह गुण है जो किसी भी स्थिति में, execution से पहले, बाद में और उसके दौरान भी हमेशा true रहना चाहिए
• उदाहरण के लिए double-entry bookkeeping का accounting equation एक प्रतिनिधि invariant है (कुल credit = कुल debit)
• अगर पूरे कोड को छोटे चरणों में बाँटकर यह साबित किया जाए कि हर चरण invariant को बनाए रखता है, तो पूरे सिस्टम की integrity सुनिश्चित की जा सकती है
• invariants बनाए रखने के लिए listeners या lifecycle methods का उपयोग किया जा सकता है (जैसे C++ के constructors/destructors, React का useEffect)
• जब बदलाव कम हों या paths सरल हों, तब invariants की जाँच बहुत आसान हो जाती है

पृथक्करण (Isolation)

• अच्छे software की एक मुख्य विशेषता यह है कि वह मौजूदा सिस्टम को अस्थिर किए बिना नए features जोड़ या बदल सके
• कोड बदलाव के ‘blast radius’ को समझना और संरचनात्मक ‘firewall’ बनाकर उसके फैलाव को न्यूनतम रखना चाहिए
• वास्तविक service Nerve के उदाहरण में, query planner और query executor की सीमा को स्पष्ट रखने और बदलाव को उस सीमा के पार न जाने देने वाले design का परिचय दिया गया है
• अनावश्यक बदलाव-प्रसार रोकने पर verification और maintenance आसान होते हैं और stability बढ़ती है
• यह OCP(Open-Closed Principle) की उस सोच से भी मेल खाता है, जिसमें मौजूदा behavior बदले बिना functionality बढ़ाई जाती है

आगमन विधि (Induction)

• बहुत से programs में recursive functions या recursive structures शामिल होते हैं, और इनके लिए तर्क स्थापित करने में induction बहुत शक्तिशाली होता है
• recursive function के behavior और correctness को चरण-दर-चरण साबित करने के लिए base case और inductive step दोनों की जाँच करनी पड़ती है
• उदाहरण के रूप में AST (syntax tree) structure में node simplification की प्रक्रिया दी गई है, जहाँ हर चरण के inductive argument से invariant की रक्षा और सही behavior साबित किया जाता है
• जब inductive thinking स्वाभाविक बन जाती है, तो recursive code लिखना और verify करना कहीं अधिक सहज और आसान हो जाता है
• non-inductive, global (holistic) verification प्रयासों की तुलना में कौन-सा तरीका अधिक स्वाभाविक है, इस पर विचार किया जा सकता है

Proof-affinity (प्रमाण-मैत्री) नाम का एक quality metric

• लेखक यह तर्क रखते हैं कि वह कोड अच्छा है जिसके बारे में दिमाग में छोटे-छोटे प्रमाण बनाए जा सकें
• अगर कोड में monotonicity, immutability, स्पष्ट conditions, invariants का विभाजन, firewall boundaries, और induction जैसी संरचनाएँ हों, तो उसे वास्तव में prove करना आसान हो जाता है, और इसी वजह से कोड की quality भी बढ़ती है
• अगर कोड समझने में कठिन हो और उसे verify करना मुश्किल लगे, तो यह refactoring या संरचना पर दोबारा विचार करने की आवश्यकता का संकेत है
• इस संदर्भ में लेखक ‘provability’ के बजाय ‘proof-affinity’ शब्द प्रस्तावित करते हैं
• proof-affinity software quality का एकमात्र तत्व नहीं है, लेकिन कोड को समझने, बढ़ाने, test करने और maintain करने में यह बहुत महत्वपूर्ण catalyst है

कौशल बढ़ाने के तरीके

• ऐसी तार्किक सोच अभ्यास के साथ इतनी विकसित होती है कि बाद में यह अवचेतन रूप से स्वाभाविक लगने लगती है
• (mathematical) proofs लिखने का नियमित अभ्यास और logical reasoning विकसित करना आवश्यक है
• algorithm problems सुलझाना (जैसे Stanford के EdX lectures, Leetcode आदि) भी अच्छा प्रशिक्षण है; खासकर उन समस्याओं पर ध्यान देना अधिक उपयोगी है जिनमें केवल tricks नहीं बल्कि सावधानीपूर्ण implementation और proof-oriented thinking चाहिए
• बार-बार परिणाम सुधारते हुए उत्तर तक पहुँचने के बजाय, एक ही प्रयास में सही उत्तर के क़रीब पहुँचने का अभ्यास महत्वपूर्ण है
• ऐसी आदतें विकसित करने से logical system design और code quality में बड़ा सुधार आता है

[GN⁺]

Hacker News राय

• इस विषय पर बिल्कुल फिट बैठने वाला, सरल लेकिन चौंकाने वाला उदाहरण है: binary search। left/right variants भी हैं, लेकिन अगर loop invariant के बारे में न सोचें तो इसे सही तरह से implement करना बहुत मुश्किल है। इस लेख में invariant-based approach और उसके अनुरूप Python code example समझाया गया है। Programming Pearls के लेखक Jon Bentley ने IBM programmers से साधारण binary search implement करने को कहा था, और 90% implementations में bug था। ज़्यादातर गलती infinite loop में फँसने की थी। उस समय integer overflow को भी खुद संभालना पड़ता था, इसलिए कुछ हद तक समझ आता है, लेकिन फिर भी यह अनुपात चौंकाने वाला है

  • इसे देखकर मैंने interview question के रूप में binary search का इस्तेमाल शुरू किया। जाने-माने candidates में से लगभग 2/3 लोग 20 मिनट के भीतर सही चलने वाला implementation नहीं कर पाए। खासकर आसान cases में infinite loop में फँसने की घटनाएँ बहुत थीं। जो सफल हुए, उन्होंने जल्दी implement किया। समस्या के कारणों में से एक यह है कि बहुतों ने गलत interface के साथ सीखा होता है। Wikipedia में भी "L को 0 और R को n-1 से initialize करें" जैसा वर्णन है, जो R-inclusive range है। व्यवहार में, ज़्यादातर string algorithms में upper bound को include न करने वाला रूप, यानी R = n, ज़्यादा बेहतर होता है। मैं इस hypothesis को सीधे experiment करके देखना चाहता हूँ। अलग-अलग function prototypes और initial values के साथ बहुत लोगों से इसे लिखवाकर inclusive और exclusive upper bound, तथा length-based approaches में bug rate की तुलना करना दिलचस्प होगा

  • सच कहें तो binary search index management के लिहाज़ से लगभग सबसे पेचीदा प्रतिनिधि उदाहरण है। Hoare partition algorithm के साथ मिलाकर देखें तो यह उन बुनियादी algorithms में है जिन्हें बिना गलती के बिल्कुल सही code करना सबसे कठिन होता है

  • मैंने test के तौर पर Claude Sonnet से bug-free binary search Python code लिखवाया

  def binary_search(arr, target):
      left = 0
      right = len(arr) - 1
      while left <= right:
          mid = left + (right - left) // 2
          if arr[mid] == target:
              return mid
          elif arr[mid] < target:
              left = mid + 1
          else:
              right = mid - 1
      return -1
  

  और example array पर कई test cases भी जाँचे गए

  • मुझे पता था कि binary search bugs गलत best practices के लिए मशहूर हैं, इसलिए मैंने सोचा कि किताब में bug-free पहला implementation छापने की चुनौती लूँ। मैंने बहुत सावधानी से लिखा, फिर भी उसमें bug निकल आया, जो अब सोचकर मज़ेदार लगता है। शुक्र है Manning के pre-publication feedback system की वजह से print होने से पहले उसे ठीक किया जा सका

  • मैं left/right binary search implementations हमेशा "अब तक का सबसे अच्छा value" याद रखते हुए लिखता हूँ। यह C++ के lower_bound, upper_bound जैसे तरीके के करीब है। while (l < r) संरचना में midpoint निकालकर current position check करते हैं और उसके अनुसार range को adjust करते हैं। उदाहरण के लिए upper_bound में left boundary बढ़ाते हैं, और lower_bound में right boundary घटाते हैं। काफ़ी समय बाद leetcode हल कर रहा था, इसलिए दिमाग सुस्त था और format थोड़ा बिखरा हुआ हो सकता है

• बहुत पहले graduate class में मैंने इससे मिलता-जुलता विचार सीखा था। undergraduate के आख़िरी दौर से मैं math exams सिर्फ़ pen से देने लगा था। वजह ठीक से नहीं जानता था, लेकिन marks लगातार अच्छे आते थे, क्योंकि मैं सवाल को एक ही बार में इस तरह हल करता था कि पूरा समाधान पहले दिमाग में पूरी तरह बन जाता था, फिर उसे लिखता था। इससे छोटी-छोटी गलतियाँ बहुत कम हो गईं। coding करते समय भी मैं कुछ ऐसा ही करता हूँ: पहले दिमाग में चीज़ों को काफ़ी हद तक पूरा design करके शुरू करता हूँ

• बेहतर programmer बनने के लिए code के भीतर छोटे-छोटे proofs लिखने की आदत डालनी चाहिए tests और type definitions इसी काम के उदाहरण हैं मैं खास तौर पर पहले tests, फिर types, और आख़िर में code लिखने की तरफ़ जाता हूँ हर acceptance criteria के लिए test बनाना अच्छा होता है, और ऐसे tests लिखने चाहिए जिनमें input/output स्पष्ट रूप से बताया गया हो अगर API है, तो OpenAPI या GraphQL से सभी properties और types सहित पहले specification बनाई जा सकती है। runtime पर इसी specification के आधार पर data validation भी संभव है, और यह specification खुद इस बात का proof बनती है कि app spec के अनुसार काम कर रहा है संक्षेप में, OpenAPI/GraphQL, tests और types के ज़रिए यह proof हासिल करना ज़रूरी है कि system वास्तव में इरादे के अनुसार काम कर रहा है अगर specification पहले सही तरह design कर ली जाए, तो code implementation को लचीले ढंग से बदला जा सकता है और correctness को specification से साबित किया जा सकता है code से ज़्यादा महत्वपूर्ण specification है

  • लेख में बताई गई पाँच properties एक अच्छे type system में व्यक्त की जा सकती हैं। इस तरह specification का बड़ा हिस्सा खुद code बन जाता है, और compiler correctness की गारंटी देता है। programming का भविष्य ऐसा होना चाहिए जहाँ यह approach सामान्य बात बन जाए OpenAPI और GraphQL के type systems इतने सीमित हैं कि ऐसे भविष्य तक पहुँचने के लिए शायद 50 साल और विकास चाहिए

• मैंने university में theoretical computer science की बुनियाद पढ़ी है, और इस लेख का मूल विचार मुझे सही लगता है। लेकिन इसे व्यवहार में लाना आसान नहीं है pre/postconditions के अलावा भी, loop invariant और structural induction जैसी CS proof techniques बहुत शक्तिशाली हैं loop invariant, structural induction के links के साथ UofT CSC236H lecture notes (lecture notes) की सिफ़ारिश करता हूँ

  • यह CSC236 lecture note वाकई शानदार है, और Professor David Liu भी बहुत अच्छे हैं प्रोफ़ेसर परिचय

  • अरे, UofT का ज़िक्र आ गया! अच्छा लगा

• "अपने code के बारे में दिमाग में छोटे proofs बनाना" इतना बुनियादी सिद्धांत है कि इसे लगभग self-evident होना चाहिए। code के हर हिस्से के बारे में मन में हमेशा एक छोटा proposition होना चाहिए कि यह क्या कर रहा है

  • यह बात greenfield projects में आसान लगती है, जहाँ हाल में सारा code आपने खुद लिखा हो। लेकिन असली codebases में, जहाँ कई developers अलग-अलग functions और global state को छूते हैं, यह कहीं ज़्यादा कठिन लगता है

    • सचमुच अच्छे developers की पहचान ही यह है कि वे system को धीरे-धीरे इस दिशा में ले जा सकें। वास्तविक दुनिया का code अव्यवस्थित होता है, लेकिन invariants में छेद को क्रमशः कम करना और ऐसी code structure बनाना ज़रूरी है जिसमें बाद में आने वाले developers भी invariants को समझें और उन्हें बनाए रखने के अनुकूल code लिखें। documentation मदद करती है, लेकिन मेरे अनुभव में code structure उससे भी बड़ी भूमिका निभाती है

    • दरअसल global state के ख़तरनाक होने की निर्णायक वजह यही है। code की correctness prove करनी हो तो फिर पूरे program को समझना पड़ता है। अगर global variables को immutable values में बदला जाए, या उन्हें function arguments के रूप में पास किया जाए, या wrapper class में state को समेटकर संभाला जाए, तो बस उस function के callers को स्पष्ट रूप से समझना काफ़ी होता है। अगर function के भीतर assertions आदि से और constraints जोड़ दिए जाएँ, तो proof की कठिनाई काफ़ी घट जाती है। बहुत से programmers पहले से ऐसे फ़ैसले लेते हैं, बस वे proofs को सचेत रूप से सोचकर नहीं बल्कि सहज रूप से ऐसा करते हैं

    • ऐसा code जहाँ global state को कई developers संभालते हों, उसकी तुलना "metastatic cancer" वाले मरीज़ से की जा सकती है। उसका इलाज बहुत कठिन होता है, और कभी-कभी किस्मत तथा बाहरी परिस्थितियों के सहारे ही उसे बचाया जा सकता है

    • लेख में जैसा कहा गया है, ऐसे code में bugs आने की संभावना बहुत ज़्यादा होती है, और maintenance के दौरान अतिरिक्त bugs जुड़ने की भी आशंका बड़ी रहती है। यह दिखाता है कि शुरुआत से ही proof-friendly structure में लिखना कहीं अधिक सही रास्ता है

    • यह लेख पढ़कर मुझे अपने coding style के बारे में लगातार दोबारा सोचते रहने और बेहतर दिशा में उसे फिर से परिभाषित करने की अपनी आदत याद आई। सोचता हूँ, John Carmack जैसे developers को भी क्या समय के साथ अपनी पुरानी code कमतर लगने लगती होगी, और क्या उनके भीतर भी चीज़ों को और "बेहतर" करने का ऐसा ही एहसास होता होगा

• यह विचार कि code proof-friendly होना चाहिए, पहली बार 1959 में Dekker द्वारा mutual exclusion problem हल करते समय सामने आया था। इस पर एक दिलचस्प किस्सा Dijkstra के लेख EWD1303 में है (मूल लिंक)। Dijkstra का बाद का काम भी इसी insight की निरंतरता के रूप में देखा जा सकता है

• सही proof लिखना वास्तव में बहुत कठिन है। program verification भी आसान नहीं है। मेरी राय में, अगर manually proofs लिखने बैठेंगे तो यह efficient नहीं होगा। अगर आप उस language और codebase के लिए idiomatic code लिखते हैं, तो invariants या pre/postconditions के बारे में ज़्यादा सोचने की ज़रूरत नहीं पड़ती। R. Pike और B. W. Kernighan की "The Practice of Programming" में जिस "simplicity, clarity, generality" पर ज़ोर है, उसका practical work में बहुत बड़ा असर है। थोड़ा संबंधित लेकिन अलग मुद्दा यह है कि competitive programming करने पर यह साफ़ समझ में आता है कि code correctness सुनिश्चित करने की techniques सीखे बिना अगले स्तर पर पहुँचना मुश्किल है

  • मैं इससे सहमत नहीं हूँ। मुझे लगता है कि लेखक का आशय पूर्ण formal proof नहीं, बल्कि यह है कि अपने code में कौन-सी logical properties guaranteed हैं, जैसे invariants, इस पर ज़रूर सोचना चाहिए। code को समझने और उससे जुड़ी घबराहट दूर करने का यह सबसे अच्छा रास्ता है

  • यहाँ तो cause और effect उलटे लग रहे हैं। जब आप समस्या पर सावधानी से सोचते हुए आगे बढ़ते हैं, तो परिणामस्वरूप code स्वाभाविक रूप से clear और clean बनता है। logic स्पष्ट होगी तो code design भी स्पष्ट होगा। लेकिन सिर्फ़ code को सुंदर लिख देने से correctness अपने-आप आ जाएगी, ऐसा मानना ठीक नहीं है। हाँ, code जितना साफ़ होगा, code review आदि में bugs उतने कम हो सकते हैं। ध्यान रहे, form follows function

  • proof की सबसे बुनियादी धारणा है: "यह सही क्यों है, इसका आधार क्या है"। यह केवल छोटी गलतियों से बचने का साधन नहीं, बल्कि मूल रूप से यह जाँचने की प्रक्रिया है कि दिशा ही सही है या नहीं

  • code correctness के लिए सही code लिखने के अलावा कोई विकल्प नहीं है। चाहे मुश्किल हो, इसे सही ही लिखना होगा

  • अगर पहले पैराग्राफ़ को उलटकर देखें, तो उचित abstraction, यानी language/codebase के अनुरूप idiomatic code, program verification को आसान बनाती है। उचित abstraction होने पर loop invariants आदि के बारे में अलग से सोचना नहीं पड़ता, इसलिए code की correctness से proof लगभग सीधे निकल आता है

• mutability और immutability भी महत्वपूर्ण properties हैं। state को जितना संभव हो immutable रखने से न सिर्फ़ multithreading बल्कि program state के बारे में reasoning करना भी कम जटिल हो जाता है

  • मूल लेख में यह बात पहले से शामिल है

• 80s में Carnegie Mellon में undergraduate रहते हुए मुझे यह सिद्धांत बहुत स्पष्ट रूप से सिखाया गया था। बाद में इसने मेरी ज़िंदगी में बहुत मदद की। खास तौर पर जब मैंने recursion और induction की equivalence सीखी, तब पहली बार recursive algorithms को "बस कोशिश करते रहो जब तक जवाब न मिले" वाली चीज़ के बजाय एक साफ़-सुथरे तरीके से समझना शुरू किया

  • मैंने वह class हाल ही में ली, और functional programming पढ़ते हुए यह बात और गहराई से समझ आई