गेब्रिएला मोरेरा, क्विंट के सीईओ – साक्षात्कार श्रृंखला

गेब्रिएला मोरेरा, क्विंट के सीईओ, एक शोध इंजीनियर हैं जो प्रोग्रामिंग भाषाओं और औपचारिक तरीकों में विशेषज्ञता रखते हैं, जिसमें जटिल प्रणाली सत्यापन को इंजीनियरों के लिए अधिक सुलभ बनाने पर मजबूत ध्यान केंद्रित किया गया है। वह क्विंट के विकास का नेतृत्व करती है, जो टीएलए+ पर आधारित एक आधुनिक कार्यान्वित विशिष्टता भाषा है, जहां वह भाषा और इसके टूलिंग को बनाए रखने और विकसित करने का काम करती है। उनका काम औपचारिक सत्यापन, स्थिर विश्लेषण और डेवलपर टूलिंग में फैला हुआ है, और उन्होंने अकादमिक योगदान दिया है औपचारिक तरीकों को सिखाकर, जो व्यावहारिक इंजीनियरिंग और सैद्धांतिक गहराई का मिश्रण है।

क्विंट, जिसे इनफॉर्मल सिस्टम्स में विकसित और बनाए रखा जाता है, एक आधुनिक विशिष्टता भाषा है जो वितरित नेटवर्क, ब्लॉकचेन और डेटाबेस जैसी जटिल प्रणालियों को मॉडल, परीक्षण और सत्यापित करने के लिए डिज़ाइन की गई है। टीएलए+ के आधार पर निर्मित, क्विंट एक अधिक डेवलपर-अनुकूल वाक्य रचना पेश करता है, साथ ही साथ उन्नत टूलिंग जैसे कि प्रकार जांच, सिमुलेशन और मॉडल जांच, जो इंजीनियरों को तैनाती से पहले प्रणाली विफलताओं का पता लगाने की अनुमति देता है। प्लेटफ़ॉर्म कार्यान्वित विशिष्टताओं पर जोर देता है, जो डेवलपर्स को न केवल प्रणाली व्यवहार का वर्णन करने की अनुमति देता है, बल्कि सक्रिय रूप से इसका परीक्षण और अन्वेषण भी करने की अनुमति देता है, सैद्धांतिक सही और वास्तविक दुनिया के कार्यान्वयन के बीच की खाई को पाटता है।

शुरू से शुरू करते हुए, क्या आपको प्रोग्रामिंग में रुचि जगाई, और आप औपचारिक तरीकों और वितरित प्रणालियों में कैसे पहुंचे?

मैं एक उत्साही गेमर था जिसके पास एक खराब कंप्यूटर था, और मुझे एहसास हुआ कि मुझे समस्याओं को ठीक करने और इसे काम करने में मजा आता है। मैंने कंप्यूटर विज्ञान के लिए साइन अप किया और सिद्धांत और संकलक में आकर्षित हुआ।

2015 में, मुझे प्रोग्रामिंग प्रतियोगिताओं के साथ प्रस्तुत किया गया था। उनमें, आपको आमतौर पर कुछ इनपुट और अपेक्षित आउटपुट के उदाहरण मिलते हैं, और आप समस्या का समाधान करने वाला कोड लिखते हैं जो उन उदाहरणों के लिए काम करता है। हालांकि, जब आप इसका मूल्यांकन करने के लिए प्रस्तुत करते हैं, तो कोड वास्तव में उन उदाहरणों से परे कई अधिक उदाहरणों के साथ परीक्षण किया जाता है। यह एहसास कि कोड मेरे द्वारा देखे गए या सोचे गए दृश्यों के लिए काम कर सकता है, लेकिन अभी भी मेरे द्वारा नहीं सोचे गए मामलों में विफल हो सकता है, ने प्रोग्रामिंग को एक तरह की चुनौती बना दिया जिससे मैं प्यार करने लगा।

उद्योग में काम करते हुए, मुझे जल्द ही वितरित प्रणालियों में आकर्षित किया गया, जहां हमें संदेशों के आगमन के विभिन्न क्रम, विभिन्न विफलता मोड और एक पूरे छिपे हुए व्यवहार को ध्यान में रखना था। 2018 में, एक सहयोगी ने मुझे टीएलए+ नामक एक औपचारिक विशिष्टता भाषा से परिचित कराया। मैं आकर्षित हुआ। मैंने तुरंत टीएलए+ के आसपास टूल्स बनाना शुरू कर दिया और तब से इस स्थान में काम कर रहा हूं।

आपने अपना करियर औपचारिक तरीकों और प्रोग्रामिंग भाषाओं के आसपास बनाया है, टीएलए+ पर आधारित टूलिंग से लेकर क्विंट के विकास का नेतृत्व करने तक। क्या आपको औपचारिक सत्यापन को अधिक सुलभ बनाने पर ध्यान केंद्रित करने के लिए प्रेरित किया?

टीएलए+ बहुत अच्छा है और इसका व्यापक रूप से उपयोग किया जाना चाहिए। मैं अभी भी काफी जूनियर था जब मैंने इसके बारे में सीखा, और मैं अपने सहयोगियों के साथ कॉल में शामिल होता था ताकि हम साथ में समाधान खोजने की कोशिश कर सकें, और मैं अक्सर उन दृश्यों का पता लगाने में सक्षम था जहां हमारे समाधान विफल हो सकते थे। हालांकि, मैं अक्सर उन दृश्यों के खिलाफ आखिरी रक्षा पंक्ति था। मुझे लगा कि इन दृश्यों को हल करने का एक बेहतर, कम लागत वाला और अधिक मूल्यवान तरीका होना चाहिए। इसलिए, मैंने औपचारिक तरीकों का उपयोग करके कोड लागू करने से पहले विशिष्टताओं का निर्माण करने का विचार बनाया। इसलिए, मैंने इसके लिए अपनी अकादमिक यात्रा शुरू की, जो मुझे इनफॉर्मल सिस्टम्स और क्विंट में ले गई।

क्विंट को उन लोगों के लिए डिज़ाइन किया गया है जो औपचारिक तरीकों और सामान्य सॉफ्टवेयर इंजीनियरिंग के बीच की खाई को पाटना चाहते हैं। आपने पारंपरिक दृष्टिकोण की तुलना में किन सबसे बड़े उपयोगिता बाधाओं को दूर करने का प्रयास किया?

ईमानदारी से, सबसे बड़ी उपयोगिता बाधा वाक्य रचना थी। यही कारण है कि हमने वाक्य रचना से शुरू किया। इसके बाद, हम अन्य कारकों पर ध्यान केंद्रित कर सकते थे। क्विंट की प्रकार और प्रभाव प्रणाली ने जितनी संभव त्रुटियों को झंडा दिखाने के लिए पहले से ही नियमित सत्यापन प्रक्रिया शुरू करने से पहले त्रुटियों को झंडा दिखाने के लिए डिज़ाइन किया गया था, और लोगों ने इसका बहुत मूल्यांकन किया। इससे हमें उच्च गुणवत्ता वाली विशिष्टताओं लिखने में मदद मिली जो और भी लोग पढ़ सकते थे। हमने इसे संपादकों में एकीकृत किया और मूल कार्यक्षमता प्रदान की जो सभी डेवलपर्स के लिए अपेक्षित थी।

क्विंट की एक प्रमुख ताकत इसकी क्षमता है जटिल प्रणालियों को तैनाती से पहले मॉडल और परीक्षण करने की। यह डेवलपर्स को ब्लॉकचेन या रियल-टाइम इंफ्रास्ट्रक्चर जैसी प्रणालियों के निर्माण के बारे में कैसे सोचने के तरीके को बदलता है?

सबसे बड़ा परिवर्तन सत्यापन को पहले ले जाना है। लेस्ली लैमपोर्ट, टीएलए+ के निर्माता, लिखित विशिष्टताओं की तुलना निर्माण से पहले नीले रंग के निर्माण से करते हैं। यहां तक कि अगर आपने पहले से ही कुछ बनाया है बिना नीले रंग के, तो अभी भी एक लिखना और इसका उपयोग आगे के परिवर्तनों के लिए सूचित करने के लिए एक अच्छा विचार है।

क्विंट टीएलए+ के आधार पर बनाया गया है, जो वितरित प्रणालियों का वर्णन करने के लिए व्यापक रूप से उपयोग किया जाता है। आपने सैद्धांतिक शुद्धता को बनाए रखने के साथ-साथ भाषा को अधिक डेवलपर-अनुकूल बनाने के लिए कैसे संतुलित किया?

मुख्य निर्णय टीएलए+ (टीएलए+ के पीछे की तर्क) के एक खंड को क्विंट में प्रकट करने के बजाय प्रतिबंधित करना था। टीएलए+ बहुत अभिव्यक्तिपूर्ण है, और उस अभिव्यक्तिपूर्णता में से कुछ ऑपरेटर हैं जो किसी भी टूल द्वारा समर्थित नहीं हैं, और संयोजन जो लोग समझते हैं और गलत तरीके से उपयोग करते हैं, जो वास्तव में मुश्किल हो जाता है डीबग करने के लिए। हमने एक जानबूझकर निर्णय लिया: उन चीजों के साथ चिपके रहें जिनकी वास्तविक विशिष्टताओं को वास्तव में आवश्यकता होती है, और भ्रम की संभावना को避ाएं।

आपने स्थिर विश्लेषण और प्रकार प्रणालियों पर भी काम किया है। इन अनुभवों ने क्विंट के प्रकार जांच, टूलिंग और समग्र डेवलपर अनुभव को कैसे प्रभावित किया है?

इस दुनिया में मैंने सीखा सबसे बड़ा सबक यह है कि सभी भाषाएं समान नहीं हैं। आप लोगों को यह कहते हुए सुनेंगे कि यह केवल एक नई वाक्य रचना सीखने की बात है, सभी एक ही अवधारणाएं अभी भी लागू होती हैं, इसलिए सभी भाषाएं समान हैं और यह केवल स्वाद की बात है। यह सच नहीं है। प्रोग्रामिंग भाषाओं के क्षेत्र में महान शोधकर्ता हैं जो इस क्षेत्र को आगे बढ़ाने के लिए अद्भुत काम करते हैं, और यह केवल भाषा को अधिक आकर्षक या अपनी पसंद के अनुसार बनाने के लिए नहीं है।

आपने औपचारिक तरीकों को एक लेक्चरर के रूप में सिखाया है। आज औपचारिक सत्यापन के बारे में इंजीनियरों के बीच सबसे आम गलत धारणाएं क्या हैं?

मैं उन छात्रों को सिखा रहा था जो उद्योग में अभी शुरू हो रहे थे। उनके अधिकांश ने पहले कभी औपचारिक तरीकों या औपचारिक सत्यापन के बारे में नहीं सुना था, इसलिए कोई गलत धारणा नहीं थी! पाठ्यक्रम इस तरह से बनाया गया था कि उनमें से अधिकांश ने वितरित प्रणालियों या थ्रेड्स के बारे में भी नहीं सीखा था, और उनमें से आधे ने उसी सेमेस्टर में सीखा था। मैं उन्हें बता रहा था कि मैं उन्हें यह सिखा रहा था कि एक छतरी का क्या उपयोग है इससे पहले कि उन्होंने बारिश का अनुभव किया हो!

सॉफ्टवेयर विकास के साथ एआई को जोड़ने में बढ़ती रुचि है। क्या आप औपचारिक विशिष्टताओं को लिखने, सत्यापित करने या甚至 क्विंट जैसे टूल का उपयोग करके जनरेट करने में एआई की भूमिका देखते हैं?

एक महत्वपूर्ण एक, और यह पहले से ही हो रहा है। कंप्यूटर विज्ञान लिखने से बड़ा है कोड, और एआई पूरी तरह से नए तरीकों को खोलता है जिसमें हम औपचारिक तरीकों का उपयोग कर सकते हैं। एलएलएम क्विंट विशिष्टताओं को प्राकृतिक भाषा विवरण से और यहां तक कि मौजूदा कोड से भी लिखने में सक्षम हैं। क्विंट एलएलएम किट में क्लाउड कोड एजेंट हैं जो एक प्रोटोकॉल के अंग्रेजी विवरण से एक क्विंट विशिष्टता उत्पन्न करते हैं जिसे आप तुरंत चला और जांच सकते हैं।

आगे देखते हुए, औपचारिक तरीकों को निचे अपनाने से मानक सॉफ्टवेयर विकास जीवन चक्र का हिस्सा बनने के लिए क्या होने की आवश्यकता है?

क्विंट के लिए दो उच्च-स्तरीय चीजें जो मुझे पता हैं कि अधिक ग्रहण के लिए आवश्यक हैं: कम लागत और उच्च मूल्य। मुझे लगता है कि यह कई अन्य चीजों पर भी लागू होता है। औपचारिक तरीकों को हाल ही में दोनों में एक बड़ा बढ़ावा मिला है, एआई ने औपचारिक विशिष्टताओं को लिखने की लागत को बहुत कम कर दिया है और ऐसा वातावरण बनाया है जहां औपचारिक तरीके सबसे अधिक प्रभावी और मूल्यवान हो सकते हैं।

एआई हमारे पेशे को बदल रहा है, कम से कम कुछ हद तक, मुझे उम्मीद है कि यह परिवर्तन उच्च-स्तरीय डिजाइन निर्णयों और व्यवहार की सही ढंग से हमारी ओर जाता है, औपचारिक तरीकों को एक दैनिक उपकरण बनाता है; और न कि हमें समझने में असमर्थ कोड की समीक्षा करने में हमारा समय बिताने के लिए, बिना किसी टूलसेट के जो हमें इसके बारे में कारण देने में मदद करे।

साक्षात्कार के लिए धन्यवाद; पाठक जो जटिल प्रणालियों के लिए मॉडलिंग और सत्यापन के लिए इस कार्यान्वित विशिष्टता भाषा के बारे में अधिक जानने में रुचि रखते हैं, इसके टूलिंग और शुरू करने के तरीके के बारे में क्विंट का अन्वेषण कर सकते हैं।