‏استدلال محلی، تضمین سراسری؛ درسی از Rust

نویسنده که سال‌ها کارش طراحی زبان برنامه‌نویسی بوده، می‌گه چند وقته ازش می‌پرسن آیا هوش مصنوعی به زبان‌های جدید احتیاج داره؛ اولش جوابش «احتمالاً نه» بوده چون AI تقریباً به هر زبونی کد تولید می‌کنه. ولی حالا نظرش عوض شده: به تجربهٔ اون، مدل‌ها کدِ محلیِ باکیفیت می‌نویسن اما سرِ کدی که نیاز به فهم سراسری برنامه داره اغلب گیر می‌کنن.

نشونهٔ این ضعف رو زیاد شدنِ چک‌های دفاعیِ بی‌مورد می‌دونه. این چک‌ها به‌نظر بی‌ضرر میان، ولی باعث می‌شن تعداد حالت‌هایی که خوانندهٔ بعدیِ کد فکر می‌کنه ممکنه پیش بیاد به‌شکل نمایی زیاد شه و درک کد سخت‌تر بشه. نویسنده می‌گه شاید این مشکل به‌زودی حل شه، ولی اگه نشه، باز باید سراغ طراحی زبان بریم.

سؤال اصلی مقاله اینه: آیا نمونهٔ خوبی داریم که طراحی زبان اجازه بده با «استدلال محلی» به یه «خاصیت سراسریِ شگفت‌انگیز» اطمینان پیدا کنیم؟ جوابش برنامه‌نویسی چندنخی (multi-threaded) تو Rust ـه. نویسنده تعریف می‌کنه که سایت شخصیش رو تک‌نخی نوشته بوده و برای رفع کندی، بازنویسی چندنخی‌اش کمتر از ۵ دقیقه طول کشیده، بارِ اول درست اجرا شده و مطمئن بوده که درست کار می‌کنه؛ چیزی که تو زبون‌های دیگه براش کابوس بوده.

راز کار اینه که Rust با ترکیب ownership و دو trait به اسم Send و Sync، data race ها (خوندن/نوشتن هماهنگ‌نشده که دو نخ همدیگه رو خراب می‌کنن) رو به خطای زمان کامپایل تبدیل می‌کنه. Send یعنی «این نوع رو می‌شه به نخ دیگه منتقل کرد» و Sync یعنی «چند نخ هم‌زمان می‌تونن ازش بخونن». مثال ساده اینه که وقتی یه مقدار رو با move به نخ دیگه می‌فرستی، مالکیتش هم می‌ره و اگه دوباره تو نخ اصلی بهش دست بزنی، کامپایلر جلوت رو می‌گیره:

fn main() {
    let x = vec![1, 2];
    std::thread::spawn(move || println!("{x:?}")).join().ok();
    println!("{x:?}");
}

این کد خطای «borrow of moved value: x» می‌ده. نویسنده نشون می‌ده حتی نوع‌هایی مثل Rc (شمارش مرجع غیراتمی) اجازهٔ رفتن به نخ دیگه رو ندارن و باید از Arc (شمارش مرجع اتمی) استفاده کنی. نکتهٔ عمیق‌ترش اینه: برنامه‌نویس فقط با نگاه به کدِ محلی (بدون بررسی کل برنامه) مطمئن می‌شه که هیچ data race ای تو کل برنامه ممکن نیست؛ یعنی استدلال محلی، یه خاصیت سراسری رو تضمین می‌کنه. به گفتهٔ نویسنده، اگه AI تو دیدِ سراسری ضعیف بمونه، همین‌جور طراحی‌ها می‌تونن مسیر آیندهٔ زبان‌ها باشن.

نکات کلیدی:

• AI کدِ محلی رو خوب می‌نویسه ولی تو درک سراسری برنامه ضعیفه
• نشونهٔ این ضعف، انفجار چک‌های دفاعی غیرضروریه
• تو Rust، مالکیت و trait های Send/Sync باعث می‌شن data race خطای کامپایل شه
• نتیجه: استدلال محلی یه خاصیت سراسری (نبود data race) رو تضمین می‌کنه