Concoqtion (Coq + MetaOCaml) - क्यों छोड़ा गया?

Question

ओकैमल मेलिंग सूची पर लोगों को बग करने से पहले, मैंने सोचा कि मैं यहां अपना प्रश्न पोस्ट कर सकता हूं। मैंने अभी यह beauty (Concoqtion वेबसाइट से लिंक) की खोज की है। Concoqtion MetaOCaml का एक विस्तार है जो अनुक्रमित प्रकारों (और शायद बहुत अधिक) की अनुमति देता है।

type ('n:'(nat),'a) listl = 
    | Nil : ('(0),'a) listl 
    | Cons of let 'm:'(nat) in 'a * ('(m),'a) listl : ('(m+1),'a) listl 

कि (m+1) प्रकार स्तर पर किया जाता है: इसके साथ, इस सूची में किस प्रकार का भी सूची की लंबाई में शामिल हैं बनाने के लिए आसान है। बहुत साफ़।

हालांकि, अंतिम संस्करण 2007 (ओकैमल 3.08) से है। क्या किसी को कोई विचार है कि इस परियोजना को रद्द क्यों किया गया, या अगर आज ओकैमल के लिए कुछ समान है?

Answer 1

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

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

मैं यह नहीं कहूंगा कि कॉन्कोक्शन को "त्याग दिया गया" था, बल्कि यह हमें एक सबक सिखाया गया था, लेकिन वास्तव में इसका उपयोग नहीं किया गया था। शोधकर्ताओं ने उस क्षेत्र में काम करना जारी रखा, और इस प्रणाली को कई लोगों को वर्णित किया जा सकता है (या कम से कम कुछ विचारों का पुन: उपयोग करना), उदाहरण के लिए VeriML।

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