Tôi đang làm việc trên đặc tả Concrete v2. Phiên bản đầu tiên đã có mã hoạt động và chúng tôi đã học được rất nhiều từ việc triển khai nó. Bây giờ tôi đã thêm một số tính năng thú vị mới đến từ Zig, Austral, Lean/Coq. Tôi đang thiết kế một ngôn ngữ hệ thống xung quanh xác minh hình thức ngay từ đầu với một số tính năng thú vị. Các tính năng: - hạt nhân được hình thức hóa trong Lean 4 - kiểu tuyến tính (theo kiểu Austral, không phải kiểu affine của Rust) - mượn mà không cần chú thích vòng đời - khả năng theo dõi hiệu ứng - bộ cấp phát được truyền dưới dạng khả năng (theo kiểu Zig) - mặc định là thuần khiết - ! cho các hàm không thuần khiết (từ Roc) Cách chúng kết hợp: Các kiểu tuyến tính là nền tảng. Mỗi giá trị được tiêu thụ chính xác một lần. Không có rò rỉ, không có giải phóng đôi, không sử dụng sau khi giải phóng. An toàn bộ nhớ mà không cần GC. Nó dài dòng hơn nhưng cụ thể và rõ ràng hơn so với các kiểu affine. Mượn làm cho tính tuyến tính có thể sử dụng. Tham chiếu tạm thời một giá trị mà không tiêu thụ nó. Các vùng từ vựng thay vì chú thích vòng đời của Rust. Trình biên dịch suy diễn những gì Rust yêu cầu bạn viết. Khả năng theo dõi hiệu ứng. Một hàm đọc tệp khai báo nó. Một hàm cấp phát khai báo nó. Không có khai báo có nghĩa là không có hiệu ứng, được đảm bảo. grep với(Network) tìm mọi hàm chạm vào mạng. Bộ cấp phát dưới dạng khả năng làm cho việc cấp phát trở nên rõ ràng. Mã không có with(Alloc) chứng minh rằng nó không bao giờ chạm vào heap. Bạn kiểm soát bộ cấp phát nào phục vụ cho đường dẫn mã nào. Arena, pool, cấp phát ngăn xếp, tất cả đều rõ ràng. Mặc định là thuần khiết đảo ngược mô hình thông thường. Các hiệu ứng yêu cầu khai báo. Trường hợp phổ biến (tính toán thuần khiết) không cần chú thích. Hạt nhân Lean kết nối mọi thứ lại với nhau. Khi trình biên dịch nói rằng chương trình của bạn an toàn, tuyên bố đó được hỗ trợ bởi chứng minh.