Bend 2 và những cạm bẫy của việc vibe-coding bằng AI trong thiết kế ngôn ngữ lập trình
Một bài viết kỹ thuật chỉ trích ngôn ngữ lập trình Bend 2, cho rằng việc phụ thuộc quá nhiều vào phương pháp vibe-coding bằng AI đã dẫn đến việc tái tạo các mô hình kiểm chứng chính thức (formal verification) một cách kém tối ưu. Tài liệu của mã nguồn mở này cũng ghi rõ rằng 99% trình biên dịch được viết bởi AI và chưa được kiểm toán hoàn chỉnh. Trường hợp này nêu bật rủi ro gia tăng khi sử dụng AI tạo sinh để xây dựng các hệ thống chuyên ngành mà thiếu sự nghiên cứu chuyên sâu, dễ dẫn đến các lựa chọn kiến trúc cồng kềnh hoặc kém hiệu quả. Đây là bài học cảnh báo quan trọng cho các kỹ sư phần mềm khi tận dụng LLM để thiết kế ngôn ngữ lập trình và trình biên dịch phức tạp. Những người chỉ trích chỉ ra rằng Bend 2 đòi hỏi các đặc tả và chứng minh toán học quá dài dòng, bỏ qua các thực hành hiện đại đã được thiết lập trong kiểm chứng chính thức. Tuy nhiên, các cuộc thảo luận trực tuyến lưu ý rằng mặc dù bài viết cho rằng nhà phát triển không biết đến kiểm chứng chính thức, tác giả dự án trước đó đã bàn luận rất nhiều về chủ đề này trên mạng xã hội.
## KIẾN THỨC NỀN
Vibe-coding là một quy trình phát triển phần mềm trong đó các nhà phát triển sử dụng kỹ thuật viết câu lệnh (prompt) với các mô hình ngôn ngữ lớn để tự động tạo mã nguồn. Kiểm chứng chính thức (formal verification) là một lĩnh vực trong khoa học máy tính sử dụng các kỹ thuật toán học để chứng minh rằng một chương trình đáp ứng chính xác đặc tả kỹ thuật về hành vi của nó.