Bend 2 و Vibe-Coding Trap

Bend فقط به عنوان یک مثال مفید از نکته کلی من در مورد کدگذاری vibe عمل می کند، زیرا اخیرا برجسته است و جنبه هایی دارد که استفاده از آن را به عنوان مثال آسان می کند. من هیچ چیز در مورد تاریخچه نویسنده با زبان های طراحی نمی دانم یا اینکه آیا آنها واقعا معاوضه های زیر را در نظر گرفته اند و به نظر من انتخاب ضعیفی بوده است. به راحتی می توانید «نویسنده» را با «نویسنده فرضی که می توانسته همان چیزی را خلق کرده باشد» جایگزین کنید.

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

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

بیایید با یک خط پایه از آنچه که Bend از برنامه‌نویس می‌خواهد برای نسخه نمایشی خود در صفحه اصلی بنویسد شروع کنیم:

https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend

من آن را در اینجا بازتولید نمی کنم زیرا کد خیلی مهم نیست. آنچه برای این مقاله مهم است این است که کمی کد است. این 58 خط کد است فقط برای بیان اینکه بازیکن هرگز نمی تواند پرچم را لمس کند یا بازی را برنده شود. مشکلات دیگری نیز وجود دارد که LLM می‌تواند زیربرنامه‌های Game را برای انجام هر کاری دوباره تعریف کند. با این حال، این بار دیگر هدف مقاله نیست.

در ادامه اجازه می‌دهیم ببینیم LLM که کد این برنامه را می‌نویسد، برای اثبات "قوانین" چه چیزی باید بنویسد:

https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend

این خیلی است. 442 خط کد برای اثبات این خصوصیات ساده.

خب مشکل من با این چیه؟ چرا من آن را تله کدنویسی لرزه ای می نامم؟

مشکل اینجاست که کدنویسی vibe این امکان را فراهم می‌کند که قبل از یادگیری کافی در مورد مشکل برای تشخیص وجود راه‌حل بسیار بهتر، یک راه‌حل اساسی بسازید. یک توسعه‌دهنده می‌تواند یک زبان و کامپایلر کامل را تولید کند، در حالی که رویکردی را که یک بررسی مقدماتی از این زمینه می‌توانست مستقیما در مقابل آنها قرار دهد، از دست می‌دهد.

فیلد مورد نظر تأیید رسمی است. قابل توجه است که این دو کلمه در هیچ کجای صفحه وب Bend یا در پایگاه کد آن ظاهر نمی شوند. توسعه‌دهنده یک زبان کامل را در اطراف یک فیلد ایجاد کرده است، به‌ظاهر بدون اینکه متوجه باشد که این فیلد وجود دارد.

برای اینکه به وضوح نشان دهیم که چرا این یک مشکل است، بیایید همان برنامه ای را که Bend به عنوان نسخه نمایشی در SPARK، یک زبان منبع باز و کامپایلر برای تأیید رسمی استفاده می کند، دوباره ایجاد کنیم. منصفانه در مورد Bend، من این را کاملا با vibe کدنویسی کردم، فقط به یک LLM گفتم که نسخه آزمایشی را در SPARK بدون هیچ راهنمایی بیشتر بازسازی کند:

بنابراین اکنون ما همان قوانینی را داریم که به عنوان Bend تعریف شده است، هدف من در اینجا چیست؟

تفاوت این با Bend این است که آنچه ما در اینجا ارائه کرده‌ایم همه چیز مورد نیاز برای اثبات درستی برنامه است، بدون اینکه زمان LLM و نشانه‌هایی برای ایجاد یک اثبات خطی 442 از اصول اولیه داشته باشیم. ما می توانیم GNATprove را اجرا کنیم و دریافت کنیم:

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

این مثال فراتر از Bend اهمیت دارد، vibe-coding اجرای طرحی را که به طرز وحشتناکی شکسته است یا دهه‌ها از وضعیت فعلی هنر عقب است بسیار آسان می‌کند، زیرا می‌توانید فورا بدون نیاز به تحقیق به نتیجه برسید. اگر از یک LLM زبانی بخواهید که در آن بتوان با ایجاد یک اثبات از اصول اولیه ثابت کرد که یک تابع به طور رسمی صحیح است، با خوشحالی این کار را انجام می دهد، هرگز به شما پیشنهاد نمی کند که کامپیوترها می توانند از قبل بدون نیاز به LLM اثبات های پیچیده بسازند و 99٪ کار را حذف کنند.

هرگز به شما نمی گوید که آنچه می سازید، بیشتر به عنوان کاری وجود دارد که می توانید روی آن بسازید.