Ngôn ngữ lập trình Bend: Tăng tốc GPU, tối ưu hiệu năng và ngăn chặn lỗi code từ AI

1. Cài đặt

2. Thêm nội dung này vào tệp AGENTS.md của bạn

3. Tận hưởng các ứng dụng được viết theo phong cách "vibe-coded", nhanh chóng và không có lỗi!

một ngôn ngữ tốc độ cao giúp ngăn chặn các lỗi AI thông qua chứng minh

Tốc độ như C · Song song hóa CUDA · Các chứng minh Lean

Trong nền kinh tế hậu AGI, con người cuối cùng sẽ ngừng viết và đọc mã nguồn, nhưng chúng ta vẫn cần một phương thức không gây mơ hồ để truyền đạt những gì mình muốn cho các AI đang xây dựng thế giới xung quanh chúng ta.

Với các "luật" (laws), ý định của chúng ta có thể chính xác hơn nhiều so với ngôn ngữ tự nhiên. Với các chứng minh, chúng ta có thể xác thực rằng AI đã thực hiện các câu lệnh (prompts) của mình một cách chính xác. Và một trình biên dịch nhanh sẽ giúp chạy mã đó với tốc độ tối ưu.

Đó chính là Bend - và không gì khác ngoài nó.

1. Bend chạy RẤT NHANH.

Bend biên dịch ra mã máy (native code). Trên một nhân, nó chạy nhanh gần bằng C. Cùng một tệp nhị phân đó cũng có thể chạy trên mười sáu nhân, hoặc trên GPU, với tốc độ nhanh gấp hàng trăm lần so với một nhân.

2. Bend biên dịch RẤT NHANH.

Trình kiểm tra kiểu (type checker) của Bend cũng là một trình kiểm tra chứng minh, tương tự như trong Lean và Rocq. Những trình kiểm tra này có thể mất vài phút trên một cơ sở mã nguồn cỡ trung bình. Bend chỉ mất tối đa một giây, vì vậy một tác nhân AI có thể kiểm tra sau mỗi lần thay đổi.

3. Bend hỗ trợ SONG SONG.

Không cần luồng (threads), không cần khóa (locks), không cần viết nhân (kernels). Chỉ cần chia công việc làm đôi, Bend sẽ phân bổ các lệnh gọi đến mọi nhân mà nó tìm thấy, sau đó hợp nhất chúng lại. Bây giờ hãy xem pow2 chạy trên 4.096 nhân GPU:

4. Bend NGĂN CHẶN lỗi - bằng chứng minh

Làm thế nào bạn có thể tin tưởng vào mã nguồn mà bạn chưa bao giờ đọc? Bằng cách yêu cầu một chứng minh. LAWS.bend là nơi bạn khai báo các luật. Kể từ đó, không một AI nào có thể đưa ra dù chỉ một dòng mã vi phạm các luật này. Hãy xem nó bảo vệ một trò chơi như thế nào:

Luật: không thể giành chiến thắng

Tính năng mới:

“Claude, hãy làm cho bảng trò chơi có thể cuộn vòng”

Nếu không có LAWS.bend:

Với LAWS.bend:

Nếu không có LAWS.bend, lỗi đã được đưa vào thực tế. Với LAWS.bend, AI buộc phải thử lại cho đến khi nó xây dựng được một bức tường và chứng minh rằng luật vẫn được giữ vững. Việc hợp nhất một lỗi vào mã nguồn là điều bất khả thi về mặt toán học: đó là một định lý.

LAWS.bend

PROOF.bend

LAWS.bend chính là AGENTS.md được hỗ trợ bởi chứng minh. "Không được phép có lỗi" giờ đây đã được kiểm tra kiểu.

Bạn hoài nghi ư? Hãy thử phá trò chơi này xem.

5. Bắt đầu.

5.1. Cài đặt

5.2. Yêu cầu tác nhân của bạn sử dụng Bend

Thêm nội dung này vào tệp AGENTS.md của bạn:

Sau đó, chỉ cần nói: "use Bend"!

5.3. Tận hưởng các ứng dụng được viết theo phong cách "vibe-coded", nhanh chóng và không có lỗi!

Gợi ý: hãy yêu cầu nó viết các luật cho bất cứ thứ gì không bao giờ được phép hỏng, và song song hóa mọi thứ bạn muốn chạy nhanh. Bend vẫn còn non trẻ: nếu có bất cứ điều gì sai sót, hãy yêu cầu nó mở một issue. Bend hoạt động tốt nhất trên back-end, trên Linux và macOS. Chúc bạn vui vẻ! <3

6. Tài liệu tham khảo.

Hướng dẫn: GUIDE.md là toàn bộ ngôn ngữ; lệnh "bend guide" sẽ in ra nội dung này. Bài báo: BendTT, một lý thuyết kiểu phụ thuộc affine, cốt lõi của Bend. Bài báo: BendRT, một runtime song song cho CPU và GPU, chính là máy ảo (VM) của nó.

Bend vẫn đang trong quá trình phát triển. Hãy chuẩn bị tinh thần cho các lỗi và vui lòng báo cáo chúng.