Bối cảnh xác minh hình thức cho các ngôn ngữ lập trình tiếp tục phát triển, với các công cụ như coq-of-rust nhằm chứng minh tính đúng đắn của mã theo toán học trong các ứng dụng Rust. Tuy nhiên, các cuộc thảo luận trong cộng đồng đã tiết lộ những sắc thái quan trọng về những gì xác minh hình thức có thể và không thể đảm bảo, cùng với tin tức về việc thay đổi tên đáng kể trong hệ sinh thái xác minh.
Thực tế về các tuyên bố Xác minh hình thức
Trong khi coq-of-rust hứa hẹn tạo ra các ứng dụng không có lỗi thông qua chứng minh toán học, cộng đồng phát triển đã nhấn mạnh một sự khác biệt quan trọng. Xác minh hình thức chứng minh rằng mã triển khai đúng một đặc tả, nhưng không thể đảm bảo rằng bản thân đặc tả đó không có khiếm khuyết.
Tôi thích xác minh hình thức. Nhưng tôi cho rằng đây là một sự diễn giải sai về những gì nó cung cấp. Nó cho phép bạn chứng minh về mặt toán học rằng mã của bạn triển khai đúng một đặc tả. Nó không chứng minh rằng đặc tả của bạn không có lỗi & không có lỗ hổng. Nó không chứng minh rằng đặc tả của bạn triển khai đúng các quy tắc kinh doanh của bạn.
Sự khác biệt này giữa việc xác minh (mã có khớp với đặc tả không?) và xác thực (đặc tả có đáp ứng nhu cầu thực tế không?) thể hiện một khái niệm cơ bản trong đảm bảo chất lượng. Xác minh hình thức xuất sắc trong việc chứng minh các bất biến được duy trì cho tất cả các đầu vào có thể có, điều này đặc biệt có giá trị khi đặc tả đơn giản hơn việc triển khai, chẳng hạn như trong cơ sở dữ liệu và hệ thống tệp.
Coq trở thành Rocq: Một sự đổi tên đáng chú ý
Một phát triển đáng chú ý được đề cập trong các bình luận là trợ lý chứng minh Coq, nền tảng của coq-of-rust, đã được đổi tên thành Rocq. Theo các cuộc thảo luận của cộng đồng, sự thay đổi này là kết quả từ một cuộc khảo sát cộng đồng, trong đó khoảng 24% người dùng bày tỏ sự không thoải mái với tên gọi ban đầu, cảm thấy khó chịu hoặc lúng túng khi sử dụng trong môi trường chuyên nghiệp. Dự án hiện chính thức được gọi là Rocq và có thể được tìm thấy tại rocq-prover.org.
Việc đổi tên đã gây ra các phản ứng trái chiều, với một số người xem đây là sự phát triển chuyên nghiệp cần thiết trong khi những người khác tiếc nuối việc mất đi điều mà họ coi là chơi chữ vô hại.
Vị trí độc đáo của Rust trong Xác minh
Mô hình bộ nhớ mutable-xor-aliased của Rust làm cho nó đặc biệt phù hợp cho xác minh hình thức so với nhiều ngôn ngữ khác. Mô hình này, trong đó dữ liệu có thể là có thể thay đổi hoặc có nhiều tham chiếu nhưng không thể đồng thời cả hai, tạo ra một nền tảng mà các công cụ xác minh có thể xây dựng trên đó một cách hiệu quả hơn.
Các thành viên cộng đồng lưu ý rằng nếu không có mô hình như vậy, việc xác minh trở nên khó khăn — và không thể giải quyết trong thực tế — giống như tất cả các công cụ xác minh cho các ngôn ngữ hiện có. Điều này mang lại cho các công cụ xác minh dựa trên Rust như coq-of-rust, Verus và các công cụ khác một lợi thế tiềm năng trong không gian xác minh.
Công cụ Xác minh Hình thức cho Rust Được Đề cập trong Bình luận
- coq-of-rust: Chuyển đổi Rust sang Coq để xác minh hình thức
- Verus: Hướng đến xác minh hệ thống đầy đủ (hệ thống tệp đã được xác minh, bộ điều khiển Kubernetes)
- Creusot: Chuyển đổi từ MIR sang Why3 (và sau đó là các bộ giải quyết SMT)
- Ironclad/Gloire: Không dành riêng cho Rust, nhưng là một kernel hệ điều hành được xác minh hình thức được viết bằng SPARK/Ada
Điểm Chính Về Xác minh Hình thức
- Chứng minh mã triển khai đúng theo đặc tả
- Không chứng minh bản thân đặc tả là chính xác
- Đặc biệt hữu ích khi đặc tả đơn giản hơn việc triển khai
- Được hưởng lợi từ mô hình bộ nhớ "mutable-xor-aliased" của Rust
Các phương pháp thay thế và đối thủ cạnh tranh
Bối cảnh xác minh hình thức mở rộng ra ngoài coq-of-rust. Các thành viên cộng đồng đã nhấn mạnh một số giải pháp thay thế, bao gồm Verus cho xác minh hệ thống (được sử dụng trong hệ thống tệp đã được xác minh và các bộ điều khiển Kubernetes), và nhân Ironclad với hệ điều hành Gloire được xây dựng trên nó sử dụng SPARK và Ada.
Một số nhà phát triển bày tỏ sự quan tâm đến việc áp dụng các phương pháp xác minh tương tự cho các ngôn ngữ khác như Zig, đặc biệt là thông qua các công cụ như Zig AIR, cho thấy sự quan tâm đến xác minh hình thức trên khắp hệ sinh thái lập trình hệ thống.
Việc theo đuổi tính đúng đắn của mã được chứng minh về mặt toán học tiếp tục thu hút sự quan tâm từ các cộng đồng lập trình, mặc dù với sự hiểu biết tinh tế hơn về những gì xác minh hình thức có thể thực sự mang lại. Khi các công cụ trưởng thành và các phương pháp đa dạng hóa, khoảng cách giữa sự hoàn hảo lý thuyết và việc triển khai thực tế dần thu hẹp, ngay cả khi mục tiêu khó nắm bắt của mã không có lỗi 100% vẫn là nguyện vọng hơn là thực tế.