Formal Methods: क्या ये सिर्फ अच्छी इंजीनियरिंग प्रैक्टिस हैं? (2024)

 (brooker.co.za)
1 पॉइंट द्वारा GN⁺ 2025-01-12 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • बड़े पैमाने के, distributed, महत्वपूर्ण low-level systems में formal methods को सिर्फ correctness के लिए अतिरिक्त प्रक्रिया नहीं, बल्कि समय और लागत घटाने वाली engineering practice के रूप में देखा जाना चाहिए
  • Software में design और implementation आसानी से आपस में मिल जाते हैं, इसलिए देर से किया गया design change सीधे implementation rework और API बदलाव की लागत में बदल जाता है
  • Implementation से पहले behavior और interfaces की ठोस समीक्षा करने से bug density और production के बाद की समस्याएँ घटती हैं, और सही design तक अधिक तेज़ी से पहुँचा जा सकता है
  • तेज़ी से बदलती user requirements या UI, documentation, pricing logic जैसे formalize करने में कठिन क्षेत्रों में, पूरी तरह upfront formal design की उपयोगिता कम हो सकती है
  • TLA+, P जैसे tools design stage में optimization और constraints की समीक्षा करके correctness और performance के trade-off को घटाने में भी इस्तेमाल हो सकते हैं

अच्छी engineering practice के रूप में formal methods

  • Formal methods अच्छी software engineering practice का एक महत्वपूर्ण हिस्सा हैं
  • खासकर large-scale systems, distributed systems, और महत्वपूर्ण low-level systems पर काम करने वाले engineers के लिए इनका लागू मूल्य बड़ा है
  • यह इस premise से शुरू होता है कि engineering अंततः समय और लागत को optimize करने की गतिविधि है
    • Performance, scalability, sustainability, efficiency भी साथ में consider किए जाते हैं
  • Formal methods सस्ते या आसान नहीं हैं और हर development style में अच्छी तरह fit भी नहीं होते, लेकिन यह intuition कि वे सिर्फ लागत बढ़ाते हैं, हमेशा सही नहीं होता

लागत घटाने के दो रास्ते

  • पहला है rework में कमी
    • दूसरे engineering domains के उलट, software में design और construction अक्सर साथ-साथ होते हैं
    • Design पर्याप्त आगे न बढ़ा हो, तब भी implementation शुरू किया जा सकता है
    • यह flexibility software की strength है, लेकिन design iterations को implementation iterations में बदलकर लागत बढ़ा सकती है
  • दूसरा है change cost management
    • जब किसी API या system के customers हो जाते हैं, तो बदलाव कहीं अधिक महंगे और कठिन हो जाते हैं
    • Hyrum’s Law के अनुसार, API users की संख्या पर्याप्त होने पर, contract में क्या है इससे अलग, हर observable behavior पर कोई न कोई निर्भर हो जाएगा
  • API के जरिए system behavior को isolate करना software engineering का महत्वपूर्ण idea है, लेकिन users implementation details तक पर निर्भर हो सकते हैं—यह सीमा बनी रहती है
  • API के पीछे के system को पूरी तरह reimplement किया जा सकता है, फिर भी abstraction change cost को खुद खत्म नहीं करती
  • Formal design work rework cost घटा सकता है और interface changes को पहले ही stage में handle करवा सकता है, जिससे software बनाने की speed और efficiency बढ़ती है

जिन systems में formal design अच्छी तरह fit होता है

  • यह हर software पर एक ही तरीके से लागू नहीं होता
  • जिन software में user requirements तेज़ी से evolve होती हैं या जिन्हें formalize करना कठिन होता है, उनमें upfront design का value कम हो सकता है
    • UI, websites, pricing logic implementation आदि इसमें आते हैं
    • ऐसे क्षेत्रों में लगातार rework अधिक होता है, इसलिए upfront design cost बड़ी हो सकती है
  • Agile का मूल idea implementation और requirements gathering को parallel में चलाकर release तक का time घटाना है
    • Requirements gathering जारी रहने पर भी implementation पूरा किया जा सके
    • कई मामलों में यह parallel development model optimal होता है, या progress को संभव बनाने की आवश्यक शर्त होता है
  • इसके उलट, large-scale, distributed, low-level systems के कई हिस्सों की requirements अच्छी तरह समझी हुई होती हैं
    • कम से कम sufficiently large static requirements वाला हिस्सा मौजूद होता है
    • ऐसे में upfront formal design implementation stage और production के बाद के rework तथा bug density को काफी घटा सकता है
  • Requirements जितनी अधिक physics laws जैसी होंगी, design और formal design का value उतना बढ़ेगा; और जितनी अधिक user opinions जैसी होंगी, value उतना घटेगा

Requirements documentation और formalization की सीमाएँ

  • User requirements को स्पष्ट रूप से लिखना, चाहे formal हो या informal, बहुत मूल्यवान है
  • Requirements न लिखने पर समय बर्बाद होता है, और लोग अलग-अलग दिशाओं में चलने लगते हैं जिससे friction पैदा हो सकता है
  • सभी human requirements को formally specify करना कठिन या आर्थिक रूप से उचित न हो सकता है
    • UI aesthetic requirements
    • Documentation readability
    • API naming consistency
  • Formal approach पर मतभेद इस बात से भी आते हैं कि formal approach क्या है और किस तरीके से value देती है, इस पर लोगों की अलग-अलग सोच होती है
  • UML की तरह code को विशाल diagrams में बदलने वाला तरीका, अगर कठिन सवालों से सीधे नहीं निपटता, तो उसका value कम हो सकता है
    • गलत तरीके या खराब tools से किया जाए तो valuable work भी बेकार हो सकता है

Field में उपयोगी formal methods और tools

  • Formal methods और automated reasoning एक व्यापक field हैं और इनमें तरह-तरह के tools हैं
  • बड़े cloud systems के क्षेत्र में उपयोगी रहे tool groups ये हैं
    • P, TLA+, Alloy जैसी specification languages और संबंधित model checkers
    • turmoil जैसे deterministic simulation tools
      • Fuzzing के साथ tests के जरिए state space को systematically explore करने में इस्तेमाल होते हैं
    • Dafny जैसी verification-friendly programming languages और Kani जैसे code verifiers
    • Numerical simulation techniques
    • Whiteboard या design docs में decision tables, truth tables, explicit state machines बनाने जैसी formal के करीब methods
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 lightweight formal methods को समझने की शुरुआती जगह है
  • Implementation verification ही अकेला goal नहीं है
    • TLA+ और P जैसे tools implementation से पहले design को अधिक तेज़ और ठोस रूप से review करने में बहुत value देते हैं

तेज़ software को और तेज़ी से बनाना

  • 2015 में How Amazon Web Services Uses Formal Methods लिखे जाने के समय focus मुख्य रूप से correctness पर था
    • Design की safety और liveness properties verify करना
    • सही design तक अधिक तेज़ी से पहुँचना
  • Internal lock management system में TLA+ इस्तेमाल करने वाली team के case में “aggressive optimizations को verify” करना महत्वपूर्ण था
  • TLA+ जैसे tools न केवल systems को जल्दी बनवाते हैं, बल्कि तेज़ systems बनाने में भी मदद कर सकते हैं
    • Possible optimizations को तेज़ी से explore करना
    • सच में महत्वपूर्ण constraints ढूँढना
    • Proposed optimization सही है या नहीं, यह confirm करना
  • कई मामलों में formal methods, systems में अक्सर आने वाले correctness और performance के कठिन trade-off को घटाते हैं

Design stage में इस्तेमाल होने वाले tools का value

  • System design पर सोचने में मदद करने वाले tools को design stage में इस्तेमाल करने से software development speed काफी बढ़ सकती है
  • यह risk घटाता है और शुरुआत से ही अधिक optimized system बनाना संभव करता है
  • बड़े और जटिल systems बनाने वाले engineers के लिए formal methods अच्छी engineering practice का हिस्सा हैं

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

1 टिप्पणियां

 
GN⁺ 2025-01-12
Hacker News टिप्पणियाँ

  • सॉफ़्टवेयर formal verification लेख में मानी गई बात की तरह, सॉफ़्टवेयर के प्रकार और development process पर बहुत हद तक निर्भर करता है
    formal verification इस्तेमाल करने के लिए सॉफ़्टवेयर के व्यवहार के बारे में formal requirements होने चाहिए, लेकिन ज़्यादातर projects और design philosophy इसके मुताबिक नहीं होते। अगर यह भी साफ़ न हो कि क्या चाहिए, और development व design साथ-साथ आगे बढ़ रहे हों, तो formal methods लागू करना मुश्किल होता है। लेकिन छोटे और safety-critical systems जैसे, जहाँ पहले से specification पर निर्भरता होती है, वहाँ इससे बड़ा लाभ मिल सकता है, और aerospace software इसका प्रतिनिधि उदाहरण है

    • मुझे यह इतना niche नहीं लगा। लोग जिस cost की बात करते हैं, वह पिछले कुछ दशकों में काफी कम हुई है, और TLA+ या Alloy जैसे tools मैंने developers को एक हफ्ते के भीतर भी सिखाए हैं
      आजकल यह ऐसी skill नहीं है जिसे सीखने के लिए PhD या कई साल की research चाहिए, और basic high-level specification लिखना भी ऐसा नहीं है। model checker चलाने पर जिस system को आप model कर रहे हैं, उसके बारे में कुछ सीखने को मिलता है, और सिर्फ documentation या training के लिए भी यह उपयोगी है। formal methods की बुनियादी ताकत यह है कि यह आपको आखिर तक सोचने पर मजबूर करती है। बहुत से developers मानते हैं कि वे सिर्फ अपने दिमाग, type checker और थोड़े unit tests के सहारे concurrency algorithm implement कर सकते हैं, लेकिन model checker चलाने के बाद जब design और assumptions में गलतियाँ मिलती हैं, तो विनम्र होना पड़ता है। सोच से कहीं छोटे distributed systems बहुत हैं, और state space अक्सर formalize करके देखने से पहले के अनुमान से कहीं बड़ा निकलता है
    • यह सब या कुछ भी नहीं, ऐसा मामला नहीं है। मैं पूरी तरह specification न किए गए, बहुत product-oriented backend के साथ काम करता हूँ, लेकिन उसके कुछ हिस्सों को formally specify किया गया था
      उदाहरण के लिए, एक बहुत पेचीदा state machine पर property-based testing लगाकर यह जाँचा गया कि किसी भी अजीब input से endpoint को call करने पर भी internal state machine invalid transition न करे। आसपास के code की formal specification नहीं थी, लेकिन state machine की थी, इसलिए यह संभव हुआ, और ऐसे subtle bugs भी मिले जिन्हें पारंपरिक unit testing से कभी नहीं पकड़ा जा सकता था
    • “formal” का मतलब है “ऐसी language में लिखा गया जिसे computer interpret कर सके”, और programmers का काम मूल रूप से यही है। code लिखना program behavior की formal specification लिखना है, और परिभाषा के अनुसार हर software को ऐसा करना ही चाहिए
      लेकिन formal methods का लाभ पाने के लिए program behavior की तुलना program itself के अलावा किसी और चीज़ से करनी होती है, और वह दूसरी चीज़ भी formal language में लिखी होनी चाहिए। आप जो behavior चाहते हैं उसे ठीक-ठीक समझना ज़रूरी है, लेकिन software के पूरे behavior को पूरी तरह cover करना ज़रूरी नहीं। automated unit tests भी formal specification हैं, और उन्हें चलाना formal verification method है। बस यह आम तौर पर formal methods कहे जाने वाले तरीकों की तुलना में कमजोर specification और कमजोर verification हैं; conceptually या practically इनमें कोई साफ़ गुणात्मक फ़र्क नहीं है। जिस software पर testing लागू की जा सकती है, उस पर अधिक समृद्ध formal specification methods भी लागू किए जा सकने की संभावना काफ़ी होती है, और cost-effectiveness आम तौर पर testing सीखने की तरह trial and error से सीखी जाती है
    • चाहें या न चाहें, requirements तो बनकर रहेंगी। फर्क सिर्फ इतना है कि उन्हें requirements engineering चरण में खोजकर एक साधारण text document से validate किया जाए और conflicts सुलझाए जाएँ, या coding के दौरान गलत चीज़ बन जाने के बाद पता चले, या “sprint review” में customer उन्हें पकड़ ले
      आखिरकार सवाल यह है कि “agile” कहलाने के लिए आप कितना ज़्यादा पैसा और समय खर्च करना चाहते हैं। विडंबना यह है कि पारंपरिक requirements चरण इन तीनों तरीकों में सबसे सस्ता है, और क्योंकि इसमें customer के साथ तेजी से convergence उस चरण में होता है जहाँ बदलाव की लागत सबसे कम होती है—यानी text की एक पंक्ति बदलने के स्तर पर—इसलिए यह असल agile spirit से भी सबसे ज़्यादा मेल खाता है
    • मूल बात pre-design से ज़्यादा formalizability के करीब लगती है। उदाहरण के लिए, insurance claim automation system को शुरू से design नहीं किया जा सकता, क्योंकि insurers का व्यवहार अक्सर explicitly specified नहीं होता, लेकिन interactions के ज़रिए जानकारी लेते हुए automation system को परिष्कृत किया जा सकता है
      फिर भी यह लाभ मिलता है कि आप जाँच सकते हैं कि कहीं कोई case छूटा तो नहीं, और system के भीतर कोई contradiction तो नहीं है

  • फ़ॉर्मल मेथड्स के बारे में अक्सर यह तर्क दिखता है कि “software बड़ा, जटिल और सही बनाना कठिन है, इसलिए formal methods”
    एक तरफ़ मैं चाहता हूँ कि यह सच हो। अकादमिक ढंग से सीखने वाली चीज़ों में मेरी व्यक्तिगत रुचि है, और व्यावहारिक रूप से भी यह निराशाजनक होता है कि software सचमुच जटिल होने के कारण fail हो जाए और फिर कारण ढूँढते फिरना पड़े। लेकिन formal methods इस समस्या को कैसे हल करते हैं, यह विश्वसनीय ढंग से दिखाने वाले उदाहरण बहुत कम मिलते हैं। यह लेख आधुनिक “design” के अधिकांश हिस्से को समय की बर्बादी बताने के मामले में बेहतर है, लेकिन TLA, UML से क्यों बेहतर है, यह पर्याप्त रूप से नहीं समझाता। बात कुछ ऐसी लगती है मानो आप TLA में कुछ महीने या कुछ साल लगा दें तो कोई बोध हो जाएगा, और जिसने वह बोध नहीं पाया उसे इसकी उपयोगिता समझाई नहीं जा सकती। calculus या Bayesian statistics में भी ऐसा पहलू है, इसलिए यह असंभव बात नहीं है, लेकिन अंत में फिर वही project manager वाली सोच लौट आती है: “अगर यह सच में इतना उपयोगी होता, तो ज़्यादा लोग इसका इस्तेमाल करते और इसके फायदे अपने-आप दिखते।” अगर कोई चीज़ लंबे समय से मौजूद है लेकिन व्यापक रूप से स्थापित नहीं हो पाई, तो संभव है कि उसके पीछे कोई कारण हो

    • मुझे लगता है UML बेकार होने का कारण यह है कि एक ही diagram को अलग-अलग लोग अलग तरह से समझते हैं, और यह बहुत जटिल होने के बावजूद जाँच योग्य नहीं है, इसलिए आप ऐसे UML diagram बना सकते हैं जो self-contradictory हों या जिनका कोई मतलब ही न हो
      जब किसी कठिन समस्या से सामना होता है, तो हम कोई न कोई “method” अपनाते हैं। अगर बात communication protocol की हो, तो उसे state machine के रूप में समझाना अच्छा होता है, और TLA उस niche में बेहतर फिट बैठता है। हाल के समय में ऐसे बहुत कम मसले रहे हैं जो उस स्तर की मेहनत को justify करें, लेकिन जब ऐसे मसले आते हैं तो इसकी कीमत बहुत बड़ी होती है। domain-specific language में भी यही बात लागू होती है; कई तरह की समस्याओं से बचना हो तो parser खुद लिखने के बजाय parser framework का उपयोग करना कहीं बेहतर है। आजकल ज़्यादातर rework requirements बदलने और इस वजह से आता है कि ग्राहक को असल में क्या चाहिए, यह उसे खुद स्पष्ट नहीं होता और वह बस कहता है “यह नहीं।” इसमें यह भी कारण है कि request करने वाले लोग अपनी ज़रूरतों के निहितार्थों पर पर्याप्त सोच नहीं पाते, लेकिन उससे बड़ा कारण यह है कि अच्छी decision लेने लायक ज्ञान एक ही जगह पर्याप्त मात्रा में इकट्ठा नहीं होता
    • formal methods व्यापक रूप से इस्तेमाल नहीं होते, इसका कारण शायद यह है कि ऐसे business domain वास्तव में बहुत ज़्यादा नहीं हैं जहाँ domain logic की शुद्धता को 98% से 99.99% तक ले जाने के लिए भारी समय और लागत लगाना सही ठहरे
      formal methods निश्चित रूप से बड़ा investment हैं। लेकिन भले ही वे सामान्य रूप से मुख्यधारा में स्थापित न हुए हों, उनके कुछ विचार आधुनिक type system में आ चुके हैं
    • मैंने formal verification को सिर्फ hardware classes के संदर्भ में देखा है, और यह programming जैसा तो लगता है, लेकिन cost-benefit पूरी तरह अलग है। physical chip बन जाने के बाद उन्हें आसानी से ठीक नहीं किया जा सकता, और design के प्रकार भी काफ़ी अलग होते हैं
      मेरा प्रभाव यह रहा कि formal verifier की कठोरता, सिर्फ इस वजह से कि उसे उचित समय और memory के भीतर खत्म होना चाहिए, design complexity पर भी सीमाएँ लगा देती है। शायद formal verification को आवश्यक बनाने की असली जीत यह हो सकती है कि “software बड़ा, जटिल और सही बनाना कठिन है” वाली समस्या को इस तरह ठीक किया जाए कि बड़े और जटिल program के साथ काम करना ही असुविधाजनक बना दिया जाए
    • अगर इस मेंढक को धीरे-धीरे उबालना है, तो TLA सिखाने के बजाय वहाँ से बुद्धि चुराकर लानी होगी। type system ने Hindley-Milner से बहुत कुछ लिया है, और वह खुद में formal partial proof का एक रूप है
      मैं property-based testing की ऐसी अगली पीढ़ी देखना चाहूँगा जो SAT या TLA तकनीकों का उपयोग करके input space को repeatable ढंग से तेज़ी से छोटा करे। parsing और code coverage के ज़रिए यह infer कर पाना चाहिए कि किसी function को 12 देना, 11 देने से अलग branch नहीं ले सकता, लेकिन -1 या 2^17 < n < 2^32 जैसे मान अलग हो सकते हैं
    • “अगर यह सच में उपयोगी होता, तो ज़्यादा लोग इसका इस्तेमाल करते” वाला तर्क किसी भी क्षेत्र में अच्छा नहीं है, और software development में तो दोगुना ख़राब है
      आज भी अधिकांश software project असफल होते हैं। यह “market failure” कम और “बनाने में failure” ज़्यादा है

  • formal methods की मोटे तौर पर दो धाराएँ हैं। एक extrinsic methods, जो code से अलग रहती हैं और आम तौर पर code की specification पर reasoning करती हैं, और दूसरी intrinsic methods, जो code के अंदर जाती हैं और code पर अधिक प्रत्यक्ष reasoning करती हैं
    ऐतिहासिक रूप से type system जैसी intrinsic methods function स्तर पर code पर reasoning करती रही हैं, जबकि Spin/P जैसे decidable model checker जैसी extrinsic methods automata जैसे formalism में व्यक्त code model को संभालती रही हैं। अभी formal methods research का एक स्वर्णकाल चल रहा है, और ऐसा लगता है कि type system की प्रगति और Verus जैसे project द्वारा आगे बढ़ाई जा रही intrinsic approach की तुलना में extrinsic methods धीरे-धीरे कम पसंद की जा रही हैं। https://github.com/verus-lang/verus

    • TLA+ जैसे tool बहुत छोटी specification language को target करते हैं, इसलिए वे अच्छी तरह काम करते हैं
      Rust जैसी बड़े footprint वाली language में यह कैसे काम करेगा, इस सवाल को मैंने देखा है, लेकिन अभी तक इसका अच्छा जवाब नहीं मिला। इस पर और पढ़ना चाहूँगा
    • linked Verus project में भी अगर सहीपन की specification सीधे लिखनी पड़ती है, तो मुझे ठीक से समझ नहीं आता कि वह भेद क्यों मायने रखता है
      यह सुनने में ऐसा लगता है कि intrinsic methods इसलिए पसंद की जाती हैं क्योंकि उनमें अलग specification लिखकर maintain नहीं करनी पड़ती, लेकिन व्यवहार में ऐसा नहीं है

  • lightweight formal methods की ओर इशारा अच्छा है। codebase के साथ-साथ proptest strategies का एक set बनाए रखना, हाथ से unit test लिखने की तुलना में बहुत बड़ा investment नहीं है, लेकिन व्यापक coverage और छोटे, समझ में आने वाले failure case की वजह से कहीं बेहतर insight देता है
    सबसे बढ़कर, यह approach सामान्य software development practices के साथ भी अच्छी तरह मेल खाती है। https://crates.io/crates/proptest

    • आजकल LLM से unit test काफ़ी बनाए जाते हैं। वे काफ़ी अच्छे बन जाते हैं, और आप उन्हें कह सकते हैं कि थोड़ा और thorough हो, जो boundary conditions याद आएँ उन्हें test करे, या किसी खास condition को handle करे
      मुझे अच्छे test लिखने के तरीक़े और उसमें लगने वाली मेहनत का कुछ अंदाज़ा है, लेकिन LLM मुझसे कहीं तेज़ी से बेहतर test बना सकता है। बार-बार और उबाऊ काम करते-करते मेरी तरह धैर्य खोने के बजाय, उसके लापरवाही बरतने की संभावना शायद कम है। software engineer के रूप में दोहराव वाले लगने वाले काम को automate करने की reflex होनी चाहिए, और documentation भी आजकल generate करके ज़्यादा बार और ज़्यादा जल्दी बनाई जाती है। LLM formal verification को अपनाने में एक छोटी क्रांति ला सकता है। सही specification बनाना उबाऊ काम है, लेकिन अगर काम करने वाला code, documentation और hints जैसा पर्याप्त context हो, तो यह LLM के लिए अपेक्षाकृत आसान काम हो सकता है। अगर specification पूरी की पूरी खुद लिखने के बजाय generate करवाई जाए और फिर उसे सरसरी तौर पर देखा जाए, तो लोग इसे करने के लिए कहीं ज़्यादा तैयार होंगे। Rust का उपयोग करना अपने-आप में यह संकेत है कि आप correctness को महत्व देते हैं, और उसका compiler formal methods के बिना भी इस बात को साबित करने के सबसे नज़दीकी tool जैसा है कि system शायद सही है। compiler या explicit type के बिना किसी language पर formal methods चढ़ाने की तुलना में यह शायद बहुत आसान होगा
    • proptest या qcheck formal methods नहीं, बल्कि randomized testing हैं

  • सॉफ्टवेयर formal verification अभी भी इतना कठिन है कि बहुत ही चरम मामलों को छोड़कर इसका उपयोग करना लाभकारी नहीं लगता। इसके विपरीत, hardware formal verification अब लगभग ऐसी चीज़ है जिसे न इस्तेमाल करने का कोई कारण नहीं है
    मैं लगातार इसे सीखने की कोशिश कर रहा हूँ, लेकिन अधिकांश सिस्टमों में लगता है कि आपको “compiler खुद लिखने वाले” स्तर का विशेषज्ञ होना पड़ता है। उदाहरण के लिए, मैंने varint encoder/decoder को prove करने की कोशिश की; 1~2 byte तक तो हो गया, लेकिन उससे आगे नहीं हुआ। मदद माँगने पर पता चला कि वजह compiler के अंदरूनी ऐसे ब्योरे थे जिन्हें समझना लगभग असंभव है, जैसे loop को अंदर ही अंदर सिर्फ 5 बार unroll किया जाता है। हाल में मैं Lean सीख रहा हूँ और वह मुझे पसंद भी आ रहा है, लेकिन फिर ऐसे दस्तावेज़ मिल जाते हैं: “Definitional equality includes η-equivalence…”. मैं Lean को नीचा दिखाने की कोशिश नहीं कर रहा; बल्कि alternatives की तुलना में इसकी documentation बेहतर लगती है

    • जानना चाहता हूँ कि क्या किसी ने FizzBee.io इस्तेमाल किया है। इसमें Python जैसी syntax है और examples भी ठीक-ठाक हैं: https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      formal methods ज़रूरी नहीं कि जटिल ही हों। समस्या यह है कि ज़्यादातर formal methods ऐसे डिज़ाइन किए गए लगते हैं मानो वे किसी professor की रुचि वाले खास विषय को दिखाने के लिए एक academic exercise हों। TLA+ भी paper लिखने की दिशा में डिज़ाइन की गई चीज़ के ज़्यादा क़रीब लगता है
    • यह डरावना दिख सकता है, लेकिन असल में ये सभी concepts बहुत सरल हैं, और संभव है कि आप इनमें से ज़्यादातर से पहले से परिचित हों

  • हल्के formal methods में एक चीज़ जो बहुत प्रसिद्ध नहीं है लेकिन मुझे पसंद है, वह है linear temporal logic का उपयोग करके trace verification: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    मूल रूप से आपको सिर्फ events log करने होते हैं, और event-driven architecture में यह लगभग मुफ़्त में मिल भी सकता है। उसके बाद आप execution trace पर Always(Locked, Implies(Eventually(Unlocked))) जैसे predicates चला सकते हैं। इसे पुराने traces पर भी लागू किया जा सकता है, और stress test या fuzzing के साथ जोड़कर state space भी explore किया जा सकता है। यह सरल, शक्तिशाली, व्यापक रूप से लागू होने वाला है, और इसमें model नहीं, सिर्फ predicates चाहिए

    • यह थोड़ा सूक्ष्म फर्क है, लेकिन यह सिर्फ system traces के किसी subset पर formula verify करता है, इसलिए यह testing के अधिक क़रीब है
      formal methods से तात्पर्य आम तौर पर system behavior के बारे में व्यापक आधार से होता है। TLA या इसी तरह के सिस्टमों में, भले ही वह वास्तविक सिस्टम नहीं बल्कि state machine हो, output एक ऐसा proof होता है कि LTL/CTL/TLA properties सिस्टम के सभी behaviors, यानी traces या trace tree, पर लागू होती हैं

  • पिछली चर्चा जून 2024 में हुई थी: https://news.ycombinator.com/item?id=40753989

  • बहुत धीमा। planning जल्द ही fossilization बन जाती है, और कोई भी document agile अदालत में आपके ख़िलाफ़ सबूत के रूप में इस्तेमाल किया जा सकता है

    • अगर उकसाने वाले अंदाज़ में कहें, तो यदि कभी “real agile” मिल जाए तो formal methods उसका ठीक उल्टा होगा। क्योंकि जो चीज़ें provable और reproducible हों, वे सच्चे believers के लिए ईशनिंदा जैसी हैं

  • formal methods पर मैंने जो ज़्यादातर लेख पढ़े हैं, वे consultants के potential customer acquisition जैसे लगते हैं
    यह अपने-आप में ठीक है, लेकिन जब कोई ऐसा बर्ताव करे मानो उसने formal methods के ज़रिए ज्ञान प्राप्त कर लिया हो, और कहे कि अगर आप अपने employees या colleagues के लिए training package खरीद लें या मुझे hire कर लें, तो मैं आपकी बुरी, यहाँ तक कि गैर-जिम्मेदाराना और ख़तरनाक programming habits ठीक कर दूँगा — तब वह असहज लगता है। जब formal methods सच में ऐसा high-quality code पैदा करने लगें जो specification से भटक ही न सके, तब फिर बात करें

    • https://en.wikipedia.org/wiki/SPARK_(programming_language) कैसा रहेगा
    • “ऐसा high-quality code पैदा करना जो specification से भटक न सके” उपयोगी होगा, लेकिन एक बुनियादी समस्या है। code बहुत ज़्यादा specific होता है
      formal specification में आम तौर पर इतना सूक्ष्म विवरण नहीं दिया जाता; वहाँ सिस्टम के सामान्य behavior को specify किया जाता है। इसलिए एक ही specification अक्सर कई सूक्ष्म रूप से अलग programs के अनुरूप हो सकती है। यही वजह है कि code दस्तावेज़ के रूप में कमज़ोर पड़ता है। उससे यह पता नहीं चलता कि क्या एक इरादतन चयन था और क्या संयोगवश लिया गया चयन। high-level requirements समझाने के लिए code बहुत specific होता है। इसके विपरीत, specification के विरुद्ध program verify करना ज़्यादा व्यवहार्य लगता है

  • मौजूदा formal methods समर्थकों में कुछ लोग ऐसे हैं जो formal methods का उपयोग न करने वालों को “आलसी” या “मूर्ख” मानते हैं, और अपने को इसलिए श्रेष्ठ दिखाना चाहते हैं कि वे “सही काम” कर रहे हैं या “जटिल भाषाओं में निपुण” हैं
    बेशक सभी ऐसे नहीं हैं, और मैं अच्छे लोगों को भी जानता हूँ, लेकिन कुछ लोग वास्तव में one-trick pony के अधिक क़रीब हैं। अगर आप उनसे पूछें कि हाल के वर्षों में उन्होंने कौन-से दूसरे formal methods systems सीखे या आज़माए हैं, तो वे कहते हैं कि वे इतने “व्यस्त” हैं कि कुछ नया सीख नहीं सकते। हाल के, अधिक उपयोग में आसान formal methods में FizzBee है, जो Python dialect का उपयोग करता है और pseudocode की तरह पढ़ा जाता है; Quint है, जिसकी syntax आसान है; और P है, जिसकी syntax C# users को परिचित लगेगी। इस लेख के लेखक ने भी लिखा है कि formal methods उनके problem का सिर्फ आधा हिस्सा हल करते हैं: https://brooker.co.za/blog/2022/06/02/formal.html
    लेकिन वहाँ जिस समस्या की बात की गई है, उसे PRISM काफ़ी पहले से, और कोई नई चीज़ न होते हुए भी, हल कर चुका है। बस Brooker ने इधर-उधर देखना या सीखना नहीं चाहा