چرا Jane Street بعد از ۲۵ سال نظرش دربارهٔ روشهای صوری عوض شد
هوش مصنوعیخلاصهٔ کاملتر
یارون مینسکی، که سال ۲۰۰۲ به Jane Street پیوست و شرکت رو متقاعد کرد سراغ OCaml بره، میگه ۲۵ سال به همه میگفته که این شرکت بهعنوان یه سازمان به روشهای صوری (formal methods) علاقه نداره، ولی دیگه این حرف رو نمیزنه. به گفتهٔ نویسنده، این به این معنی نیست که اون سالها اشتباه میکردن؛ اونها همیشه به قدرت ابزارها برای نوشتن کد بهتر و قابلاعتمادتر باور داشتن و سیستمهای تایپ رو هم یهجور روش صوری سبک میدونن که کلی ازش سود بردن. ولی جدا از چند مورد خاص مثل سنتز سختافزار، حسشون این بود که روشهای صوری کامل بهصرفه نیستن.
نویسنده هزینهٔ بالا رو با مثال seL4 توضیح میده؛ یه microkernel که بهطور صوری اثبات شده و یه دستاورد بزرگه، ولی خیلی گرون تموم شد: ۲۵ نفر-سال کار برای اثبات ۸۷۰۰ خط کد C، و هر خط کد حدود ۲۳ خط اثبات و نصف روز-نفر زمان میخواست. به گفتهٔ نویسنده، این رویکرد برای یه microkernel امنیتیحساس که ریسکش بالاست شاید بصرفه، ولی برای بیشتر نرمافزارها و حتی بحرانیترین کدهای خود اونها منطقی به نظر نمیاومد.
اما ظهور کدنویسی ایجنتی نگاهشون رو عوض کرده. نویسنده میگه این موضوع از دو جهت معادله رو به هم میریزه. اول از سمت هزینه: مدلها نمیتونن خودشون بهتنهایی اثباتهای دلخواه و سخت بسازن، ولی خیلی کمک میکنن و دایرهٔ کسایی که میتونن مولد از این ابزارها استفاده کنن رو گستردهتر میکنن. دوم از سمت فایده: حالا که مدلها کد مفید زیادی تولید میکنن، یه شکاف بزرگ بین کدی که مدل میسازه و کدی که واقعاً بخوای منتشرش کنی وجود داره. نویسنده میگه کد ایجنتی هنوز به سمت «slop» میل داره؛ بیشازحد پیچیده، پر از باگهای عجیب و گوشهوکنارهای خاص، و اغلب پایبند به ناورداییهای اصلی کدبیس نیست.
به گفتهٔ نویسنده، آدمها مجبورن وقت زیادی صرف راستیآزمایی کد تولیدشده توسط ایجنتها بکنن، و روشهای صوری میتونن بخشی از این بار رو سبک کنن و فرایند بازبینی رو خیلی کارآمدتر کنن. جدا از این، ایجنتها روی فیدبک رشد میکنن؛ چه موقع آموزش با یادگیری تقویتی و چه موقع کدنویسی. روشهای صوری یه شکل قدرتمند دیگه از فیدبک هستن که توان ایجنتها برای حل مسائل سخت رو بالا میبرن. البته تستها هم خیلی ارزشمندن، مخصوصاً تستهای مبتنی بر ویژگی و fuzzing، ولی تستها محدودیت ذاتی دارن و نمیتونن همهٔ فضای حالت برنامه رو پوشش بدن. نویسنده اشاره میکنه که توی OxCaml دیدن ایجنتها از تضمینهای سراسری (همون ∀ که از سیستم تایپ میگیری) خیلی سود میبرن؛ مثلاً اگه سیستم تایپ جلوی data race یا آسیبپذیری XSS رو بگیره، میتونی کاملاً از شرشون خلاص بشی، کاری که تست بهتنهایی بهسختی از پسش برمیاد.
نویسنده میگه Jane Street دو برگ برنده داره: کنترل عمیق روی زبانی که استفاده میکنه (که اجازه میده زبان رو برای تکنیکهای اثباتمحور بهتر کنه، مثل افزودن مشخصههای ماژولار به سیستم تایپ یا محدودیتهای سطح-تایپ روی مالکیت و تغییرپذیری) و یه جامعهٔ برنامهنویس که آمادهٔ این کاره. به گفتهٔ اون، توی بیشتر جاها سختترین بخش متقاعد کردن آدمها به استفاده از ایدههای جدیده، ولی توی Jane Street کاربرها از اینکه قابلیتهای جدید سیستم تایپ بهاندازهٔ کافی سریع نمیان عصبانی میشن. حالا شرکت داره یه تیم میسازه و برای لندن و نیویورک نیرو میگیره؛ امیدشون اینه که روشهای صوری به همون اندازه که سیستمهای تایپ پیشرفته براشون مفیدن، به ابزاری فراگیر برای ساخت نرمافزار تبدیل بشه.
نکات کلیدی:
- Jane Street بعد از ۲۵ سال بیعلاقگی، داره یه تیم برای روشهای صوری میسازه
- دلیل تغییر نظر: کدنویسی ایجنتی هم هزینهٔ این ابزارها رو پایین آورده هم فایدهشون رو بالا برده
- کد تولیدشده توسط ایجنت اغلب به سمت «slop» میل داره و راستیآزماییاش وقتگیره
- روشهای صوری هم بار بازبینی رو سبک میکنن هم به ایجنتها فیدبک قوی میدن
- کنترل عمیق روی OxCaml و یه جامعهٔ آمادهٔ کاربر، Jane Street رو برای این کار مناسب میکنه
