"برنامه‌نویسی با طعم شیرین اثبات"
———————————————

یکی از آرزوهام اینه که اگر یه روزی استاد دانشگاه شدم، یکی از دروسی که حتما درس بدمش درس مبانی برنامه‌نویسی باشه. به‌نظرم یکی از مناسب‌ترین جاها برای اینکه بشه به یک ذهنی ساختار و شکل داد، زمانیه که ذهن خالی از هرگونه دیدگاه و اندیشه‌ی خام و نارس باشه. یعنی همون اول کار ذهن طرف جوری شکل بگیره که تا آخر عمر دعات کنه. جای اینکه ذهنش پر بشه از کلی سینتکس و پارادایم‌هایی که براش کلی تناقض و بی ثباتی ایجاد میکنه، ذهنش رو سازماندهی کنی تا نظمی مستحکم استوار بشه. خلاصه خوابای زیادی دیدم برای اون روز :)))

قطع به یقین سیلابس اون درس، برپایه‌ی Curry–Howard isomorphism خواهد بود، بدون اینکه دانشجوها متوجه این قضیه بشن یا دردی احساس کنن :))) ممکنه بپرسید چرا چنین تصمیمی دارم و اصلا این چیزی که گفتم بدون درد و خون‌ریزی معنیش چیه.
بذارید کمک‌تون کنم. آقای Haskell Brooks Curry که به احترام ایشون، زبان برنامه‌نویسی Haskell، زبان برنامه نویسی Curry و زبان برنامه‌نویسی Brooks رو از روی نام ایشون انتخاب کردند، به همراه آقای Wiliam Howard یک رابطه‌ای کشف کردند که به Curry–Howard isomorphism معروفه. این رابطه به زبان ساده میگه که بین logic و programming، بین Proof و Program و بین Theorems و Types یک نوع Isomorphism وجود داره. یعنی هر Type یک Theorem و هر برنامه یک اثبات هستش. حالت معوکسش هم برقراره یعنی هر اثبات یک برنامه است. طبق این رابطه، میشه اثبات کرد زمانی که شما برای هر زبان برنامه‌نویسی که از نوع statically typed یا dependent type باشه(یعنی Type ای که وابسه به Value باشه)، یک Type Checker بسازید، در اصل براش یک Theorem Prover ساختید! بنابراین میشه برنامه‌هایی که با این زبان‌ها نوشته میشن رو طبق Curry–Howard isomorphism به یک اثبات تبدیل کرد و این به ما کمک میکنه که بتونیم درستی برنامه‌ای که نوشتیم رو اثبات کنیم.

حالا شاید براتون کم کم ملموس شده باشه که چرا می‌خوام چنین کاری بکنم. میام بهشون یه زبان Functional Dependent Type یاد میدم مثل Agda، Coq یا Idris که هم برنامه‌نویسی فرمال بر اساس Lambda Calculus که یک Universal Computation Model مثل ماشین تورینگ هست رو یاد بگیرن و هم بتونن با استفاده از Theorem Proving، درستی برنامه‌ای که نوشتن رو اثبات کنن.

حالا اصلا چرا این همه براتون حرف زدم و سرتون رو درد آوردم؟

چون همین چند روز پیش متوجه شدم که تفکر بنده رو قبلا بهش رسیدن و یه پارادایم برنامه‌نویسی بر اساسش توسعه دادن به نام Proof-Oriented Programming. یعنی همون موقعی که داری Program ات رو Design میکنی، اثبات درستیش رو هم جلو ببری.

هم پیمان با این پاردایم، زبان برنامه‌نویسی ای توسعه داده شده که هم Dependent Type Functional Programming هستش و هم با استفاده از Z3 که یک Theorem Prover هستش که برا اساس SMT-Solving کار میکنه، میتونیم برنامه‌هایی که باهاش می‌نویسیم رو اثبات کنیم. این زبان F* نام داره و اولین بار در سال ۲۰۱۱ توسط تیم Prosecco در موسسه‌ی INRIA Paris توسعه داده شد. بعدها Microsoft خیلی از این زبان خوشش اومد و پروژه توسط تیم Prosecco و Microsoft Research در سال ۲۰۱۶ بازنویسی شد و ورژن فعلی زبان F* بر اساس همون پیپر ۲۰۱۶ هستش. سینتکس زبان شبیه به ML هستش(یقینا منظورم اون ML دروغین که توی ذهن‌ همه‌تونه نیست :))) ).

برنامه‌های F* به طور معمول به زبان OCaml کامپایل و اجرا میشن. البته یک سری Fragment از زبان F* هم هستن که به C و Assembly کامپیال میشن مثل Low* که یک فرگمنت از زبان F* هستش.

شما به واسطه‌ی F* می‌تونید برنامه‌ای که می‌نویسید رو از چند جهت Verify کنید. یکیش اینه که برنامه از نظر Functionality داره درست کار میکنه که این میشه همون اثبات Correctness. بحث بعدی ویژگی‌های امنیتی به طور مثال اثبات کنید که برنامه‌تون هیچ وقت دیتا secrete رو Leak نمی‌کنه. و بحث آخر هم اثبات Lower bound و Upper Bound روی منابعی که مصرف می‌کنه.

اگر می‌خواید F* یاد بگیرید چند تا راه وجود داره. کتابی برای این زبان نوشته شده که به‌طور رایگان در دسترس عموم قرار داره و می‌تونید فایل PDF اش رو از اینجا دانلود کنید. از طریق این لینک هم می‌تونید به صورت Web-based این کتاب رو بخونید. خوبیشم اینه که همواره آپدیت میشه.

تعدادی هم مینی کورس بر اساس این زبان ساخته شده می‌تونید توی صفحه‌ی اصلی زبان، توی بخش Course Material به منابع این کورس ها اعم از Lecture Notes ها و کدها دسترسی پیدا کنید.