Góc nhìn từ Bend 2: Cái bẫy của 'Vibe Coding' và sự lãng phí khi tái phát minh bánh xe

18 tháng 9, 2026

[Bend chỉ đóng vai trò là một ví dụ hữu ích cho quan điểm chung của tôi về vibe-coding vì nó mới, nổi bật và có những khía cạnh giúp dễ dàng sử dụng làm ví dụ. Tôi không biết gì về lịch sử thiết kế ngôn ngữ của tác giả, hoặc liệu họ có thực sự cân nhắc những đánh đổi dưới đây và đưa ra lựa chọn mà tôi cho là kém tối ưu hay không. Bạn cứ thoải mái thay thế cụm từ “tác giả” dưới đây bằng “một tác giả giả định có thể đã tạo ra cùng một thứ”.]

Bend 2 đang được quảng bá như một ngôn ngữ dành cho kỷ nguyên lập trình AI: con người viết các “luật” (laws), AI viết các triển khai và chứng minh, còn trình biên dịch sẽ kiểm tra tính đúng đắn của các chứng minh đó. Tất cả nghe có vẻ khá ấn tượng và tôi có thể hiểu tại sao ai đó lại muốn một ngôn ngữ làm được điều này. Thực tế có một vài vấn đề lớn với ý tưởng này; tuy nhiên, đó không phải là nội dung của bài viết này. Thay vào đó, tôi muốn nói về việc bản thân Bend dường như đã rơi vào một cái bẫy phổ biến của vibe-coding mà tôi không thấy được nhắc đến nhiều.

Hãy bắt đầu với cơ sở về những gì Bend yêu cầu nhà phát triển viết cho bản demo trên trang chủ của nó:

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

Tôi sẽ không sao chép lại ở đây vì mã nguồn không quá quan trọng. Điều quan trọng đối với bài viết này là nó khá dài. Phải mất 58 dòng mã chỉ để tuyên bố rằng người chơi không bao giờ được chạm vào lá cờ hoặc thắng trò chơi. Ngoài ra còn có những vấn đề khác khi LLM có thể định nghĩa lại các chương trình con Game để thực hiện bất cứ điều gì; tuy nhiên, đó một lần nữa không phải là trọng tâm của bài viết.

Tiếp theo, hãy xem LLM cần viết những gì để chứng minh các “luật” này cho chương trình:

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

Con số đó rất lớn. 442 dòng mã chỉ để chứng minh những thuộc tính đơn giản đó.

Vậy vấn đề tôi gặp phải ở đây là gì? Tại sao tôi lại gọi nó là cái bẫy vibe-coding?

Vấn đề là vibe-coding giúp bạn có thể xây dựng một giải pháp đáng kể trước khi tìm hiểu đủ về vấn đề để nhận ra rằng vẫn còn một giải pháp tốt hơn nhiều. Một nhà phát triển có thể tạo ra toàn bộ một ngôn ngữ và trình biên dịch trong khi bỏ lỡ một phương pháp mà nếu chỉ cần khảo sát sơ bộ về lĩnh vực này, họ đã có thể thấy ngay trước mắt.

Lĩnh vực đang được nhắc đến là kiểm chứng hình thức (formal verification). Đáng chú ý là hai từ này không xuất hiện ở bất kỳ đâu trên trang web hay trong codebase của Bend. Nhà phát triển đã xây dựng cả một ngôn ngữ xoay quanh một lĩnh vực mà dường như họ không hề biết đến sự tồn tại của nó.

Để chứng minh rõ ràng tại sao đây lại là một vấn đề, hãy tái tạo lại cùng một chương trình mà Bend sử dụng làm demo trong SPARK, một ngôn ngữ và trình biên dịch mã nguồn mở dành cho kiểm chứng hình thức. Để công bằng với Bend, tôi đã hoàn toàn sử dụng vibe-coding cho việc này, tôi chỉ yêu cầu LLM tái tạo bản demo trong SPARK mà không đưa ra hướng dẫn gì thêm:

Vậy bây giờ chúng ta đã có các luật được định nghĩa giống như Bend, quan điểm tôi muốn đưa ra ở đây là gì?

Điểm khác biệt so với Bend là những gì chúng ta cung cấp ở đây là tất cả những thứ cần thiết để chứng minh tính đúng đắn của chương trình, mà không cần để LLM lãng phí thời gian và token vào việc xây dựng một chứng minh dài 442 dòng từ các nguyên lý cơ bản. Chúng ta có thể chạy GNATprove và nhận được kết quả:

Tác giả của Bend đã hoàn toàn bỏ lỡ việc đây là tiêu chuẩn hiện tại trong lĩnh vực kiểm chứng hình thức, nếu họ thậm chí biết lĩnh vực này tồn tại. Thay vào đó, họ đã tạo ra cả một hệ thống yêu cầu các đặc tả dài dòng và các chứng minh còn dài dòng hơn nữa. Một chút nghiên cứu trước khi vibe-coding toàn bộ ngôn ngữ và trình biên dịch có thể đã cải thiện đáng kể kết quả vì tác giả sẽ biết mình cần yêu cầu những gì.

Ví dụ này quan trọng vượt ra ngoài phạm vi của Bend, vibe-coding khiến việc triển khai một thiết kế bị lỗi nghiêm trọng hoặc lạc hậu hàng thập kỷ so với công nghệ hiện tại trở nên quá dễ dàng, bởi vì bạn có thể nhận được kết quả ngay lập tức mà không cần phải thực hiện bất kỳ nghiên cứu nào. Nếu bạn yêu cầu LLM tạo ra một ngôn ngữ có khả năng chứng minh một hàm là đúng đắn về mặt hình thức bằng cách xây dựng chứng minh từ các nguyên lý cơ bản, nó sẽ vui vẻ thực hiện điều đó; nó sẽ không bao giờ dừng lại để gợi ý cho bạn rằng máy tính đã có thể tự xây dựng các chứng minh phức tạp mà không cần đến LLM và loại bỏ 99% khối lượng công việc. Nó sẽ không bao giờ nói với bạn rằng những gì bạn đang xây dựng thực chất đã tồn tại dưới dạng các công trình mà bạn có thể kế thừa và phát triển.