गैब्रिएला मोरेरा, क्विंट की सीईओ – इंटरव्यू सीरीज

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

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

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

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

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

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

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

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

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

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

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

पाठकों के लिए जो इसके साथ परिचित नहीं हैं, आप क्विंट को कैसे समझाएंगे और मौजूदा टूल्स जैसे टीएलए+ के साथ एक नई विनिर्देश भाषा की आवश्यकता क्यों है?

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

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

टीएलए+ हमेशा ऐसा कर सकता था। क्विंट इसे उन इंजीनियरों के लिए व्यावहारिक बनाता है जो पहले से ही समयिक तर्क में विशेषज्ञ नहीं हैं।

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

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

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

मेरे लिए टीएलए+ सyntax के साथ सबसे बड़ा दर्द बिंदु यह था कि मैं कितनी बार अपने बैकस्लैश और नियमित स्लैश को मिलाता था, और आपको उन्हें बहुत बार टाइप करना होता है। मुझे क्विंट की सyntax बहुत पसंद है, लेकिन जो वास्तव में मुझे वापस जाने से रोकता है वह सभी टूलिंग है।

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

हम एलएलएम का उपयोग भाषा टूल के रूप में करते हैं जो प्राकृतिक भाषा के इरादे से क्विंट के सटीक परिभाषाओं को लिखते हैं, और फिर क्विंट टूल्स को एआई को देते हैं ताकि वे उन चीजों को कर सकें जो वे स्वयं पर भरोसा नहीं कर सकते हैं, जैसे कि किनारे के मामलों को खोजना।

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

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

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

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