هیلل وین: AI متدهای فرمال رو فراگیر نمی‌کنه
تست
هوش مصنوعیخلاصهٔ کامل‌تر
هیلل وین، مشاور و مدرس متدهای فرمال و نویسندهٔ کتاب Logic for Programmers، مهمون این قسمت بوده. بحث از یه پیش‌بینی رایج شروع میشه: چون AI داره بیشتر کد رو می‌نویسه، لابد formal verification (یعنی اثبات ریاضی اینکه سیستم دقیقاً همون کاری رو می‌کنه که تو مشخصات گفته شده) بالاخره فراگیر میشه. جواب وین به این پیش‌بینی منفیه.
محور فنی گفت‌وگو TLA+ ـه، زبان مشخصه‌نویسی که لزلی لمپورت ساخته. مدل TLA+ ماشین حالت سیستم رو توصیف می‌کنه، بعد ابزار از حالت اولیه شروع می‌کنه و همهٔ حالت‌های قابل‌دسترس رو می‌گرده تا ببینه خاصیت‌هایی که از قبل تعریف کردی همه‌جا برقرارن یا نه. برگ برندهٔ معروفش AWS بوده: تیم AWS باگی پیدا کرد که کوتاه‌ترین رد خطاش ۳۵ قدم بود و قبلش از دیزاین‌ریویو، کد ریویو و تست سالم رد شده بود.
پس چرا همه‌جا ازش استفاده نمی‌کنیم؟ به گفتهٔ وین چون نوشتن spec تو دنیای واقعی کابوسه. حتی مسئلهٔ سادهٔ «فایلی رو تو یه پوشه پیدا کن که بیشترین تعداد خط رو داره» وقتی فرمال مدل بشه باید جواب بده که ASCII یا UTF-8، فایل غیرقابل‌خوندن چی میشه، symlink چی. بدون متدهای فرمال میشه یه راه‌حل ساده نوشت که تو بیش از ۹۹٪ موارد درسته؛ متد فرمال کلی کار اضافه می‌خواد برای همون کمتر از ۱٪ حالت عجیب.
توصیهٔ عملی‌اش برای بیشتر مهندس‌ها property-based testing ـه: به‌جای نوشتن ورودی‌های نمونه، خاصیت‌هایی رو تعریف می‌کنی که همیشه باید برقرار باشن و ابزار هزاران ورودی بهش می‌ده. به نظر وین این سبک‌ترین شکل متد فرمال و عملی‌ترین راه برای ساختن نرم‌افزار مقاومه. یه باگ هم هست که حسابی اذیتش می‌کنه: فاصلهٔ بین لحظهٔ چک کردن و لحظهٔ استفاده، مثل چک کردن موجودی حساب و بعد برداشت پول.
بخش دیگهٔ گفت‌وگو مقایسهٔ مهندسی نرم‌افزار با مهندسی سنتیه. وین حدود ۲۰ نفر رو تو رشته‌های مختلف مصاحبه کرده و نتیجه گرفته که سطح دقتی که نرم‌افزار لازم داره، عنوان «مهندس» رو توجیه می‌کنه. نکتهٔ جالبش اینه که «مواد اولیهٔ» ما به‌طرز عجیبی یکدست‌ان: یه برنامه روی هر کامپیوتری یکسان اجرا میشه، ولی مهندس برق باید با مقاومتی کنار بیاد که تا ۲۰٪ اختلاف داره.
نکات کلیدی:
- TLA+ رو لزلی لمپورت ساخته و با پیمایش همهٔ حالت‌های قابل‌دسترس سیستم کار می‌کنه
- باگی که AWS با متدهای فرمال پیدا کرد، کوتاه‌ترین رد خطاش ۳۵ قدم بود
- به گفتهٔ وین، AI سهم formal verification رو نهایتاً از حدود ۰.۱٪ به ۰.۳٪ می‌رسونه
- برای بیشتر تیم‌ها property-based testing کافیه، نه متدهای فرمال کامل
- باگ time-of-check در برابر time-of-use، یعنی فاصلهٔ بین چک کردن شرط و انجام عمل، از نگرانی‌های اصلی اونه
