मैं औपचारिक सत्यापन इंजीनियर के रूप में एथेरियम में शामिल हो रहा हूं। मेरा तर्क: औपचारिक सत्यापन केवल एक दुर्लभ स्थिति में पेशे के रूप में समझ में आता है
- सत्यापन लक्ष्य छोटे, सरल नियमों (ईवीएम) का पालन करता है;
- लक्ष्य में बहुत अधिक मूल्य (Eth और अन्य टोकन) होते हैं;
- लक्ष्य सही पाने के लिए काफी पेचीदा है (कोई भी गैर-तुच्छ कार्यक्रम);
- और समुदाय जानता है कि इसे ठीक करना महत्वपूर्ण है (शायद)।
औपचारिक सत्यापन इंजीनियर के रूप में मेरी पिछली नौकरी ने मुझे इस चुनौती के लिए तैयार किया। इसके अलावा, एथेरियम के आसपास, मैं दो परियोजनाओं के साथ खेल रहा हूं: एक ऑनलाइन सेवा जिसे कहा जाता है डॉ वाई का एथेरियम अनुबंध विश्लेषक और एक जीथब रिपॉजिटरी Coq सबूत युक्त। ये परियोजनाएं स्वचालित विश्लेषक और मैन्युअल प्रूफ विकास के बीच स्पेक्ट्रम के विपरीत चरम पर हैं।
संपूर्ण पारिस्थितिकी तंत्र पर सामूहिक प्रभाव को ध्यान में रखते हुए, मैं एक कंपाइलर में एकीकृत स्वचालित विश्लेषक से आकर्षित हूं। बहुत से लोग इसे चलाएंगे और कुछ इसकी चेतावनियों को नोटिस करेंगे। दूसरी ओर, चूंकि किसी भी आश्चर्यजनक व्यवहार को बग माना जा सकता है, किसी भी आश्चर्य को हटा दिया जाना चाहिए, लेकिन कंप्यूटर मानवीय अपेक्षाओं को नहीं समझ सकते। मशीनों को मानवीय अपेक्षाएँ बताने के लिए कुछ मानवीय प्रयास आवश्यक हैं। अनुबंध डेवलपर्स को मशीन-पठनीय भाषा में अनुबंध निर्दिष्ट करने और मशीनों को संकेत देने की आवश्यकता होती है कि कार्यान्वयन विनिर्देश से मेल क्यों खाता है (ज्यादातर मामलों में मशीन अधिक से अधिक संकेत चाहती है जब तक कि मानव को बग का एहसास न हो, अक्सर विनिर्देश में)। यह श्रम प्रधान है, लेकिन ऐसे मानवीय प्रयास उचित हैं जब एक अनुबंध बहु-मिलियन डॉलर ले जाने के लिए डिज़ाइन किया गया हो।
औपचारिक तरीकों के लिए समर्पित व्यक्ति होने से न केवल हमें इस महत्वपूर्ण बल्कि फलदायी क्षेत्र में तेजी से आगे बढ़ने की क्षमता मिलती है, उम्मीद है कि पिछले हफ्तों में दिखाई देने वाली विभिन्न विलक्षण परियोजनाओं को जोड़ने के लिए हमें अकादमिक के साथ बेहतर संवाद करने की भी अनुमति मिलती है।
यहाँ कुछ परियोजनाएँ हैं जिनसे हम भविष्य में निपटना चाहेंगे, उनमें से अधिकांश शायद अन्य टीमों के सहयोग से की जाएँगी।
दृढ़ता:
- सॉलिडिटी को व्हाई3 में विस्तारित करना पूर्ण सॉलिडिटी भाषा में अनुवाद (शायद एफ* पर स्विच करें)
- सॉलिडिटी की औपचारिक विशिष्टता
- कई पार्टियों के बारे में तर्क के लिए मोडल लॉजिक्स का वाक्य-विन्यास और शब्दार्थ
समुदाय:
- एथेरियम पर औपचारिक सत्यापन परियोजनाओं का नक्शा बनाना
- स्वत: विश्लेषणकर्ताओं की बेंचमार्किंग के लिए बग्गी सॉलिडिटी कोड एकत्रित करना
- कमजोरियों के लिए ब्लॉकचैन पर तैनात अनुबंधों का विश्लेषण (संबंधित: OYENTE उपकरण)
औजार:
- ईवीएम का एक मानव- और मशीन-पठनीय औपचारिकता प्रदान करें, जिसे निष्पादित भी किया जा सकता है
- ईवीएम बायटेकोड या सॉलिडिटी में औपचारिक रूप से सत्यापित पुस्तकालयों का विकास करना
- एक छोटी भाषा के लिए औपचारिक रूप से सत्यापित संकलक विकसित करना
- अंतःक्रिया-उन्मुख भाषाओं की क्षमता का अन्वेषण करें (“यदि X होता है तो Y करें; आप केवल Z कर सकते हैं यदि आपने A किया”)
