Jane Street、AI एजेंट कोडिंग के युग में formal methods को अपनाने का निर्णय
मूल शीर्षक: Formal methods and the future of programming
यह क्यों महत्वपूर्ण है
AI कोडिंग युग में formal methods के adoption से सॉफ्टवेयर verification प्रक्रिया में क्रांतिकारी बदलाव हो सकता है।
Jane Street ने 25 साल बाद अपनी formal methods नीति बदली है। AI एजेंट कोडिंग के कारण लागत-लाभ गणना में परिवर्तन के बाद कंपनी अब formal methods टीम बना रही है। पहले seL4 जैसे महंगे प्रोजेक्ट्स को देखकर यह दृष्टिकोण था कि formal methods अधिकांश सॉफ्टवेयर के लिए उपयुक्त नहीं।
Jane Street के Yaron Minsky ने घोषणा की है कि कंपनी ने formal methods के प्रति अपना 25 साल पुराना रुख बदल दिया है। पहले कंपनी का मानना था कि formal methods की लागत बहुत अधिक है - seL4 microkernel के उदाहरण में 8,700 लाइन C कोड को verify करने में 25 person-years का समय लगा था, जिसमें प्रत्येक कोड लाइन के लिए 23 लाइन proof और आधा person-day का समय चाहिए था।
हालांकि, AI agentic coding के आने से स्थिति बदल गई है। AI models formal methods को उपयोग में आसान बना रहे हैं और अधिक लोगों के लिए accessible कर रहे हैं। साथ ही, verification की जरूरत भी बढ़ गई है क्योंकि AI द्वारा जेनरेट किए गए कोड में अक्सर bugs और complexity होती है।
कंपनी का लक्ष्य formal methods को उतना ही उपयोगी बनाना है जितना आज sophisticated type systems हैं। AI agents feedback पर अच्छा काम करते हैं, और formal methods इस feedback loop को बेहतर बना सकते हैं।