‏خودکارسازی اثبات با کمک مدل‌های زبانی

نویسنده می‌گه همیشه به زبان‌های وابسته‌نوع (dependently-typed) مثل Lean و Rocq علاقه داشته، چون سیستم نوعشون می‌تونه قواعدی رو که تو زبان‌های معمولی نهایتاً به شکل یه کامنت باقی می‌مونن، رسماً بنویسه و ماشین بررسیشون کنه. ولی به گفتهٔ اون قدرت زیاد سیستم نوع یه بهای سنگین داره: نوشتن اثبات. نویسنده به گزارش پروژهٔ seL4 اشاره می‌کنه که توش حدود ۱۰ برابر طراحی و پیاده‌سازی، وقت صرف اثبات شده و بیست برابر کد C خط اثبات نوشتن.

نکتهٔ کلیدی که مقاله روش تکیه می‌کنه «بی‌ربطی اثبات» (proof irrelevance) ـه: وقتی گزاره درست باشه، محتوای اثبات مهم نیست و فقط وجودش کافیه. نویسنده می‌گه همین ویژگی کنار مدل‌های زبانی، اون‌ها رو به یه ابزار قدرتمند برای خودکارسازی اثبات تبدیل می‌کنه و ممکنه زبان‌های وابسته‌نوع رو به‌شکل چشمگیری عملی‌تر کنه.

اون برای تجربه، یه رمزگشای فرمت فشرده‌سازی Zstandard تو Lean نوشته. بخش جالبی که توضیح می‌ده رمزگذار آنتروپیِ FSE ـه: یه ماشین حالت که تعداد حالت‌هاش از تعداد نمادها بیشتره و هر نماد به‌تناسب احتمالش سهمی از حالت‌ها می‌گیره. ترفندش اینه که برای رسیدن به تعداد بیت اعشاری، بخشی از حالت‌های یه نماد یه بیت و بخش دیگه دو بیت می‌خونن تا میانگین به عدد درست برسه؛ برای همین جدول حالت‌ها اصلاً منتقل نمی‌شه و فقط احتمال‌ها فرستاده می‌شن.

نویسنده می‌گه Lean یه زبان تابعیِ محضه مثل Haskell، ولی چند ویژگی داره که برنامه‌نویسی رو راحت‌تر می‌کنه: برخلاف Haskell سخت‌گیره (strict)، نماد do مونادیش حلقه و return و break داره، و یه بهینه‌سازی داره که تا وقتی شمارندهٔ ارجاع یه شیء یک باشه، آرایه رو درجا و کارآمد تغییر می‌ده. نمونه‌ای که می‌ذاره، تایپ یه تابعه که تضمین می‌کنه آرایهٔ برگشتی دقیقاً n بایت طول داره:

def IO.FS.Stream.readExact (st : Stream) (n : Nat) :
    IO {ba : ByteArray // ba.size = n} := …

به گفتهٔ نویسنده اوج ماجرا اونجاست که اون تونسته ویژگی‌های کلیِ تابع ساخت جدول FSE رو اثبات کنه، مثلاً این‌که جدول اندازهٔ درستی داره و برای هر نماد دقیقاً یه حالت به هر حالت مقصد می‌رسه. این همون اثبات‌های سنگینیه که سد راه استفادهٔ گستردهٔ نوع‌های وابسته بوده، ولی حالا چند مدل زبانی در حدود بیست دقیقه و با کسری از اشتراک ماهانه انجامش می‌دن. نویسنده می‌گه هرچند این روش هنوز محدودیت داره و برای همه‌چیز مناسب نیست، ولی خودکارسازی اثبات همین حالا رسیده و عملاً یه نوع تازه از زبان برنامه‌نویسی در اختیارمون گذاشته.

نکات کلیدی:

• زبان‌های وابسته‌نوع قواعد ظریف رو تو نوع‌ها رمز می‌کنن ولی اثباتشون خیلی وقت‌گیر بوده
• «بی‌ربطی اثبات» کنار مدل‌های زبانی، خودکارسازی اثبات رو ممکن کرده
• نویسنده یه رمزگشای Zstandard تو Lean نوشته و رمزگذار آنتروپی FSE رو توضیح می‌ده
• مدل‌های زبانی ویژگی‌های کلیِ الگوریتم رو در حدود بیست دقیقه و با هزینهٔ ناچیز اثبات کردن
• نتیجه اینه که یه نوع تازه از زبان برنامه‌نویسیِ عملی داره در دسترس قرار می‌گیره