Bài viết hay. Từ góc nhìn của một người từng làm xác minh chương trình, Rust có vẻ là ngôn ngữ hiện đại hữu dụng nhất để áp dụng các kỹ thuật hình thức
Các quy tắc của Rust loại bỏ rất nhiều trường hợp khó hình thức hóa. Vấn đề lớn còn lại là phân tích deadlock dưới góc nhìn thread và dưới góc nhìn Rc/borrow; hai thứ này ở mức nào đó là tương đương. Nếu Rust có phân tích deadlock tĩnh, có lẽ cả các con trỏ dereference ngược an toàn cũng sẽ khả thi; và nếu có thể chứng minh rằng mọi lời gọi borrow/upgrade đều không thất bại, thì có thể loại bỏ phần lớn reference count. Khi đó, trong những trường hợp có thể, ta cũng có được interior mutability miễn phí
Vấn đề lớn của các theorem prover là chúng được tạo ra bởi những người thích chứng minh định lý, nên dễ sa vào chủ nghĩa hình thức và lệch cảm quan UI cũng như nhu cầu của lập trình viên. Phần lớn nghĩa vụ chứng minh có thể được xử lý bằng SAT solver, nhưng các bài toán khó cần công cụ nặng hơn. Coq quá thủ công, còn người viết cho rằng ACL2 quá thiên về hàm. Machine learning có thể giúp định hướng cho theorem prover. Khó có thể giao hẳn việc chứng minh cho nó, nhưng việc suy luận proof plan trong những đoạn code có control flow và cách dùng dữ liệu nhìn chung tương tự nhau thì có vẻ khả thi
F* gần như là một ngôn ngữ thần thoại có thể tự động chứng minh giúp bạn. Nó dùng SMT solver mạnh hơn SAT, và nếu giải tự động thất bại thì vẫn có thể chứng minh thủ công
Các routine mật mã của Firefox và Wireguard không được viết bằng Rust mà bằng F*, chính xác hơn là Low*, một DSL cấp thấp được tích hợp trong F*, và đã được xác minh hoàn toàn https://project-everest.github.io/ https://mitls.org/
Đồng ý, nhưng tôi nghĩ Lean đang có bước tiến lớn về trải nghiệm người dùng trong xác minh định lý tương tác, nhờ các khả năng metaprogramming phong phú
Vấn đề khi áp dụng những công cụ như vậy để xác minh một ngôn ngữ bên ngoài như Rust là phần chứng minh không được viết bằng ngôn ngữ đích, nên lập trình viên phải học cả hai ngôn ngữ. Dựa trên kinh nghiệm viết Creusot, công việc với Verus và Aeneas, cùng kinh nghiệm tại phòng nghiên cứu Why3, tôi đã suy nghĩ về việc một “Rust có ý thức về xác minh” sẽ trông như thế nào. Nếu xây dựng một ngôn ngữ như vậy ngay từ đầu, khả năng dễ xác minh có thể được cải thiện từng bước so với cả Rust, và có lẽ đặc biệt hiệu quả ở những phần khó của chứng minh
Tôi nghĩ nhánh Coq/Agda/Lean sẽ trở thành bên thắng trong lĩnh vực chứng minh. Tương tác là một mô hình khá tốt nhờ vòng lặp phản hồi, và đây đều là các hệ thống đã tồn tại, thực sự hoạt động
Thứ tôi thấy thiếu nhất trong chức năng mặc định là một tính năng tương đương với “hãy chạy quickcheck trên chứng minh của tôi”. Khi có code và đang cố chứng minh một thuộc tính không đúng, rất dễ vò đầu bứt tai vì không hiểu tại sao không chứng minh được. Nếu trong lúc chứng minh đi tới một trạng thái vô lý, sẽ rất hay nếu có một lệnh kiểu “hãy tạo phản ví dụ tại đây” và nó trả ra phản ví dụ. Chứng minh phụ thuộc đường đi rất mạnh và nói chung không dễ, nhưng các công cụ này có vẻ đã rất gần với sự vĩ đại. Quá trình cố chứng minh code cũng cần phản ánh khả năng rằng chính code đó có thể có bug
Ý tưởng dùng machine learning để dẫn dắt theorem prover khá thú vị. Nếu hệ thống machine learning đúng, nó dẫn tới một chứng minh hợp lệ và đem lại lợi ích lớn; nếu sai thì cũng không thiệt hại nhiều
Prover sẽ không suy ra một chứng minh sai, mà chỉ thất bại trong việc suy ra một chứng minh hợp lệ. Tôi nghĩ không có nhiều ứng dụng machine learning có tính chất như vậy
Tôi không phải chuyên gia xác minh hình thức, nhưng theo tôi lock theo nghĩa truyền thống không giúp ích mấy. Không compiler nào cho ta thứ gì thực sự hữu dụng về lock; ta chỉ phải chấp nhận rủi ro và sống với nó
Thực ra trong Rust, lock và reference count là các cấu trúc runtime. Arc phá vỡ khá mạnh mô hình RAII của Rust, đến mức phải loại bỏ scoped thread, vốn yêu cầu destructor được chạy trước khi scope kết thúc. Reference count toàn cục có vấn đề về chu trình và rò rỉ, rồi lại trở thành một vấn đề mang tính toàn cục. Có lẽ khó loại bỏ hoàn toàn, nhưng tôi tin rằng tốt hơn là nhốt nó trong các scope kiểu arena. Với lock, có vẻ cần các cấu trúc dữ liệu bất đối xứng như channel. Trong Go, channel được tách thành bên gửi và bên nhận, và trong goroutine gửi có thể đặt defer close(ch); ngay cả khi panic, nó vẫn được đảm bảo chạy sau khi phần còn lại của thread kết thúc. Không nhất thiết phải là channel, nhưng nếu tách vai trò đọc-ghi/sản xuất-tiêu thụ thì việc suy luận sẽ dễ hơn nhiều và cũng có ích cho phân tích hình thức
Tôi thích việc mạch bài bắt đầu từ trích dẫn bài báo khoảng năm 1973 của Hoare và giờ đã kéo dài tới bài thứ hai. Ban đầu tôi đã viết một bình luận dài trong luồng HN về bài của boat, nói rằng việc nghiêng trích dẫn đó sang góc nhìn lấy Rust làm trung tâm là dễ hiểu xét theo nền tảng của boat, nhưng lại thu hẹp phạm vi phê phán của Hoare một cách khiên cưỡng
Giờ Grayson đã lấy mảnh hẹp đó làm điểm xuất phát để bàn về vài vùng và điểm thiết kế thú vị của Rust. Tôi vẫn nghĩ bình luận của mình là đúng, nhưng cuộc thảo luận tiếp nối từ bài của Grayson đã đủ để bù lại những bất mãn kỹ thuật của tôi với bài viết đóng vai trò điểm xuất phát
Vào khoảng giữa thập niên 1990, chính Hoare cũng đã nhận ra rằng có thể có điều gì đó sai trong nền tảng của cách tiếp cận lấy tính đúng đắn làm trung tâm kiểu thập niên 1970: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Sau đó, khi các kỹ thuật không đảm bảo tính đúng đắn nhưng tiến xa hơn kiểm thử đơn giản xuất hiện, tôi cho rằng các phương pháp không đảm bảo tính đúng đắn đã vượt lên trước các phương pháp đảm bảo tính đúng đắn
Năm 1973 là 50 năm trước, tương đương cả một đời chuyên gia. Hoare đã thực sự tiến rất gần
Ông đã tìm ra vấn đề, và nhìn lại thì lời giải ép buộc chia sẻ XOR khả biến bằng hệ thống kiểu trông như chỉ còn một bước nhỏ. Nếu khi đó người ta nhận ra bước nhỏ ấy chính là lời giải, có lẽ đã giảm được 50 năm đau đớn khổng lồ
Suy nghĩ ban đầu của tôi về trích dẫn bài báo của Hoare trong bài của boat là như sau. Sau trích dẫn đầu tiên của Hoare và phần dẫn nhập ngắn, tác giả nói rằng “khi Tony Hoare nói tham chiếu giống như lệnh nhảy, điều ông đề cập là vấn đề trạng thái vừa khả biến vừa có bí danh”. withoutboats là một nhà phát triển Rust nổi tiếng nên cách diễn giải này không gây ngạc nhiên
Nhưng bản thân trích dẫn không có vẻ củng cố góc nhìn đó. Có thể xem đây là một nỗ lực lấy lời than phiền mang tính tổng quát hơn của Hoare về chính sự tồn tại về mặt ngữ nghĩa của tham chiếu, rồi áp vào mô hình trạng thái khả biến không có bí danh của Rust để né vấn đề. Tuy nhiên, điều này gần với việc chỉ sửa một mảnh hẹp của vấn đề lớn hơn rồi nói rằng toàn bộ vấn đề đã biến mất. Những phần bị bỏ qua, đặc biệt là phần mở đầu mục “Variables” và ví dụ ALGOL 68, nghiêng mạnh hơn nhiều về phía rằng Hoare phê phán không chỉ trạng thái khả biến mà là chính khái niệm ngữ nghĩa về tham chiếu. Tôi công nhận Rust là một nỗ lực thuần hóa một phần vấn đề, nhưng không cho rằng bất kỳ ngôn ngữ nào đã “sửa xong” vấn đề này
Tôi không rõ vì sao bài này lại được khen nhiều đến vậy. Cảm giác như nhiều lĩnh vực phân tích chương trình bị gói gọn trong một đoạn văn. Tôi thích Graydon và tôn trọng quan điểm của ông, nhưng đoạn này đã đơn giản hóa quá mức
Cách giải thích rằng các ngôn ngữ có GC không mấy khi trang bị hỗ trợ suy luận cục bộ mạnh là một lập luận người rơm. Đã có những ngôn ngữ như Pony vừa đặt vùng vào hệ thống kiểu vừa dùng GC. Ngoài ra còn có cả các lĩnh vực phân tích con trỏ và phân tích thoát, vốn suy luận tính duy nhất và xác định liệu hai tham chiếu có thể là bí danh của nhau hay không. Cốt lõi của kiểu tĩnh cũng là chia heap thành các phần không phải bí danh của nhau bằng các kỹ thuật như lớp và trường. Đây không phải chuyện JavaScript, và không nên giả vờ rằng Java/C#/Scala cùng vô số ngôn ngữ GC khác không có suy luận cục bộ về trạng thái khả biến
Trong trường hợp tổng quát, không thể tự động làm việc này một cách hoàn toàn, và trên thực tế cần thứ gì đó khá giống logic phân tách. Ngữ nghĩa borrow checker của Rust cũng có thể được xem là một dạng logic phân tách giản lược
Lớp và trường không cung cấp suy luận cục bộ hoàn chỉnh về trạng thái khả biến. Lý do là lớp/đối tượng A có thể trở nên phụ thuộc vào trạng thái khả biến của lớp/đối tượng B. Kế thừa lớp kiểu Java tự nó bổ sung thêm nhiều độ phức tạp khi chương trình tiến hóa theo thời gian
Graydon không nói rằng GC khiến suy luận cục bộ mạnh trở nên bất khả thi. Ông nói rằng vì lý do nào đó, phần lớn nhà thiết kế ngôn ngữ đã đưa ra những lựa chọn đi ngược mục tiêu đó, và điều này có vẻ hiển nhiên là đúng
Tất nhiên có phản ví dụ, nhưng nhìn vào các ngôn ngữ đa dụng có GC phổ biến như Java, C#, Python thì nhận định đó đúng. Có thể diễn giải rằng ý tưởng ban đầu của hướng đối tượng gần với mô hình actor ngày nay, và chỉ muốn thay đổi các cấu trúc dữ liệu được sở hữu thông qua truyền thông điệp. Nhưng các triển khai hướng đối tượng trong thực tế gần như không tiến sát mục tiêu đó. Java không ngăn việc lưu nhiều tham chiếu khả biến tới cùng một đối tượng trong nhiều đối tượng khác nhau. Bài này giải thích điểm đó tốt hơn: https://without.boats/blog/references-are-like-jumps/
Một câu đố đơn giản: đoạn mã này sẽ in ra gì? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Chỉnh sửa: tôi đã đọc nhầm phủ định kép. Đọc lại vẫn thấy rối. Ý là Java có suy luận cục bộ, khác với JavaScript, phải không?
Tôi thường thích các bài viết của Graydon, nhưng bài này, giống như nhiều bài viết về các kỹ thuật hình thức, có thể khiến độc giả không biết lĩnh vực này hiểu lầm. Nó giống như nói rằng phương pháp biến chì thành vàng đã được cải thiện ở mức một chữ số bậc độ lớn, nhưng lại không nói rằng để đạt hiệu quả chi phí thực dụng vẫn còn thiếu 29 chữ số bậc độ lớn nữa
Việc không có alias có làm cho kiểm chứng hình thức dễ hơn đáng kể không? Đúng. Nhưng điều đó có nghĩa là ta có thể kiểm chứng các chương trình thực tế một cách thực dụng và hiệu quả về chi phí không? Hoàn toàn không. Có những chương trình, mạch và thành phần được kiểm chứng hình thức hằng ngày, nhưng chúng là ngoại lệ, tương đối rất nhỏ, và được tạo ra theo cách đặc biệt cẩn trọng. Các thuộc tính giúp suy luận cục bộ là quan trọng, nhưng chúng không tạo ra thay đổi thực chất nào trong cách bảo đảm tính đúng đắn của phần mềm chủ đạo theo một phương pháp sound
Ngay cả các chương trình trong một ngôn ngữ rất xa với tính Turing-complete — không có heap, không có con trỏ, không có số nguyên, chỉ có biến boolean và vòng lặp không thể chạy quá hai lần — cũng không thể kiểm chứng một cách thực dụng vì chúng quy về TQBF. Với một số thuộc tính, chẳng hạn an toàn bộ nhớ, thì có thể, nhưng như vậy không đủ cho những gì phần mềm cần. Trong thập niên 1970–1990 từng có hy vọng rằng dù độ phức tạp trường hợp xấu nhất là khó xử lý, các bảo đảm cục bộ và cấu trúc của ngôn ngữ sẽ giúp tránh được trường hợp xấu nhất; nhưng về sau điều đó đã được chứng minh là không đúng. Hy vọng rằng các chương trình con người thực sự viết đủ xa khỏi trường hợp xấu nhất để có thể có heuristic tốt dường như giờ cũng không còn đúng nữa
Có một bài thuyết trình liên quan đến nội dung này: https://pron.github.io/posts/correctness-and-complexity
Kết quả cốt lõi là phần lớn các thuộc tính thú vị mà ta muốn kiểm chứng không hợp thành. Ngay cả khi chứng minh được thuộc tính cho từng thành phần P1...Pn, chi phí để chứng minh thuộc tính đó cho P1 ○ ... ○ Pn không chỉ tăng siêu đa thức theo n, mà còn tăng siêu đa thức theo kích thước của từng thành phần. Nói cách khác, nó khó như khi không chia nhỏ, và tính đúng đắn không phân rã được. Vì vậy “có thể kiểm chứng khá nhiều thứ” và “những gì kiểm chứng được chỉ là một giọt nước trong đại dương” đồng thời đều đúng, và khoảng cách này thường bị bỏ qua trong các cuộc thảo luận về kỹ thuật hình thức
Trong hơn 6 năm qua, bạn đã lặp lại cùng một lập luận trên HN hàng trăm lần, và sau rất nhiều bình luận nhận được trong thời gian đó, sắc thái gần như không được bổ sung thêm
Nó không hoàn toàn sai, nhưng cũng không hoàn toàn đúng. Thật đáng ngạc nhiên là dù rất nhiều người quan tâm đến chủ đề này đã có nhiều cơ hội qua hàng trăm lần lặp lại để chỉ ra điều đó, lập trường vẫn không hề tiến hóa. Thái độ như vậy nghe như một sự khép kín bệnh lý, và khiến mọi người tham gia đối thoại lãng phí thời gian
Tôi cho rằng việc tập trung vào soundness không giúp ích cho mục tiêu phần mềm đúng đắn hơn, mà thực ra còn làm phân tán sự chú ý khỏi những kỹ thuật đã cho kết quả tốt hơn trong thực tế. Có những kỹ thuật thực dụng cũng được lý thuyết hậu thuẫn, và đôi khi còn gây ngạc nhiên cho cả những người từng nghĩ soundness là con đường duy nhất: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Chuyện như vậy lặp lại nhiều lần. Ngay cả khi các phương pháp sound có những cải tiến quan trọng, các phương pháp không sound trong thực tế vẫn đạt tiến bộ lớn hơn nhiều hướng tới phần mềm đúng đắn hơn. Một ví dụ rất gần đây là https://antithesis.com. Tất nhiên, trong một số bối cảnh cụ thể, các kỹ thuật sound có thể mạnh mẽ và thực dụng hơn, nên đây là một chủ đề phức tạp
Việc kỳ vọng rằng các thư viện Rust nhỏ có thể được kiểm chứng xem chúng dùng unsafe đúng hay không là hợp lý. Chỉ riêng điều đó thôi cũng thật sự hữu ích
Tôi cũng vừa để lại một bình luận liên quan trong bài viết về F*. Chỉ xét cú pháp thì về mặt chủ quan tôi thích F*/F# hơn Rust, nhưng với phần mềm điều khiển show đang phát triển, tôi đã quyết định dùng Ada/SPARK2014
Nếu Rust muốn thu hút những người giống như Ada/SPARK2014, nó cần một tiêu chuẩn được xuất bản chính thức như các ngôn ngữ lâu đời như C, Common Lisp, Prolog, Fortran, COBOL. Rust cũng đang bước vào lĩnh vực này khi AdaCore và Ferrous Systems hợp tác để cung cấp các công cụ kiểm chứng hình thức cho Rust tương tự Ada/SPARK2014, nhưng hiện vẫn chưa có tiêu chuẩn đã xuất bản, và di sản của Ada cùng SPARK2014 là rất lớn
Thật thú vị khi có thể xem reference counting như một dạng GC tối ưu hóa chạy tức thì, hoạt động khi dùng nghiêm ngặt cho dữ liệu không có chu trình hoặc khi có thể chấp nhận rò rỉ do chu trình. Python dùng cách kết hợp reference counting + tracing như bài viết mô tả, và tôi từng thấy các triển khai vận hành ép bộ thu gom tracing chỉ chạy một lần sau mỗi N request
Perl dùng reference counting thuần túy nhưng có weak reference, nên với cái giá là phải để ý giữ reference ở phần nào trong cấu trúc chu trình, có thể biến dữ liệu thành không có chu trình theo góc nhìn reference counting. Koka về lý thuyết dùng reference counting nhưng trên thực tế cố gắng đẩy càng nhiều càng tốt sang thời điểm biên dịch; nếu bảo đảm được rằng trong y = x + 1, x chỉ có một reference và sau đó không còn được dùng, thì có thể tái sử dụng cùng vùng lưu trữ cho y để sửa đổi tại chỗ
Nim cung cấp ORC, tức reference counting tự động cộng với một triển khai thuật toán Recycler của Bacon+Rajan. Thuật toán này được thiết kế để chỉ thu gom các chu trình trong hệ thống dựa trên reference counting, nên khá nhanh. Quay lại phía Rust, có một triển khai Recycler stop-the-world ở đây: https://github.com/fitzgen/bacon-rajan-cc và fork này được phát hành dưới dạng crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc Mục Alternative trong README có liên kết tới các thử nghiệm khác cùng lĩnh vực. Nếu khó tìm bài báo Recycler, tôi đã gom các bản sao dưới https://trout.me.uk/gc/, và nếu cùng gu thì có lẽ bạn cũng sẽ thích các bài báo dưới https://trout.me.uk/lisp/
Firefox cũng dùng reference counting cùng với bộ thu gom chu trình dựa trên trial deletion để quản lý các chu trình đi qua đối tượng DOM C++ và JS. Thực tế Graydon đã phụ trách triển khai ban đầu
Tôi cảm thấy sốt ruột với kiểm chứng hình thức chương trình. Việc chứng minh một chương trình triển khai đúng đặc tả thì về mặt lý thuyết rất thú vị, nhưng giá trị thực dụng không lớn
Viết một đặc tả đúng cũng khó như lập trình đúng, nên vấn đề khó không được giải quyết mà chỉ bị chuyển chỗ. Các phương pháp hình thức có những ứng dụng thực tế, nhưng hiếm gặp
Điều đó đúng nếu là đặc tả hoàn chỉnh, nhưng đó không phải mục tiêu thực sự. Thường thứ ta muốn chứng minh là một vài thuộc tính cốt lõi. Ví dụ hàm này luôn kết thúc, hoặc hàm kia luôn trả về một mảng đã sắp xếp
Một khi làm được việc đó, có thể ép nó thành tiền điều kiện. Ví dụ trước khi truyền một mảng vào một hàm nào đó, phải chứng minh mảng ấy đã được sắp xếp sẵn
Được viết vào ngày 15/05/2024, cũng là kỷ niệm 9 năm Rust 1.0
Tôi đã đọc bài viết được liên kết của Boats và thấy rất hay. Thật ngạc nhiên là trích dẫn của Hoare từ 50 năm trước vẫn còn liên quan, và cách diễn đạt cũng rất xuất sắc
Sẽ tốt hơn nếu có thể dùng thứ gì đó đơn giản hơn, như type guard ở thời điểm biên dịch. Khi trait bound sinh sôi, chương trình ở cấp kiểu trở nên khó đọc
Ví dụ như Where <<::Output as G>::Output as H>::Output: HList + Z hay type Output = <<::Output as G>::Output as H>::Output;. Rồi thêm Cons>>> vào đó, và nhận ra các con số như U8 của TypeNum tự thân cũng là các lớp Cons>> lồng nhau. Có thể tạo ra tiến bộ trong lĩnh vực này và khiến nó thực hiện được các kiểm chứng mong muốn, nhưng thông báo lỗi có thể khác rất xa cách lập trình viên con người viết mã, còn triển khai thì cực kỳ đau đớn
Lý do trải nghiệm lập trình viên đáng kinh ngạc là vì đây không phải “chỉ là hàm”, mà là tổ hợp của các generic cụ thể và associated type. Tôi muốn dùng kiểm tra kiểu runtime nhưng chạy ở thời điểm biên dịch; tuy nhiên để làm vậy thì phải viết mã khá khác. Rốt cuộc, làm cho Rust ở cấp kiểu/thời điểm biên dịch đơn giản hơn, mang tính hàm hơn và dễ đọc hơn có thể là con đường để các dự án phân tích hình thức kiểu này đem lại trải nghiệm tốt cho maintainer và người dùng. Tóm lại là tôi muốn comptime Rust. Và tôi cũng thắc mắc liệu Future dựa trên Pin<&mut Self> đã quá cố định rồi hay chưa. Tôi muốn thử nghiệm các triển khai nội bộ khác của async/await, nhưng không biết nên bắt đầu từ đâu
1 bình luận
Ý kiến trên Hacker News
Bài viết hay. Từ góc nhìn của một người từng làm xác minh chương trình, Rust có vẻ là ngôn ngữ hiện đại hữu dụng nhất để áp dụng các kỹ thuật hình thức
Các quy tắc của Rust loại bỏ rất nhiều trường hợp khó hình thức hóa. Vấn đề lớn còn lại là phân tích deadlock dưới góc nhìn thread và dưới góc nhìn
Rc/borrow; hai thứ này ở mức nào đó là tương đương. Nếu Rust có phân tích deadlock tĩnh, có lẽ cả các con trỏ dereference ngược an toàn cũng sẽ khả thi; và nếu có thể chứng minh rằng mọi lời gọi borrow/upgrade đều không thất bại, thì có thể loại bỏ phần lớn reference count. Khi đó, trong những trường hợp có thể, ta cũng có được interior mutability miễn phíVấn đề lớn của các theorem prover là chúng được tạo ra bởi những người thích chứng minh định lý, nên dễ sa vào chủ nghĩa hình thức và lệch cảm quan UI cũng như nhu cầu của lập trình viên. Phần lớn nghĩa vụ chứng minh có thể được xử lý bằng SAT solver, nhưng các bài toán khó cần công cụ nặng hơn. Coq quá thủ công, còn người viết cho rằng ACL2 quá thiên về hàm. Machine learning có thể giúp định hướng cho theorem prover. Khó có thể giao hẳn việc chứng minh cho nó, nhưng việc suy luận proof plan trong những đoạn code có control flow và cách dùng dữ liệu nhìn chung tương tự nhau thì có vẻ khả thi
Các routine mật mã của Firefox và Wireguard không được viết bằng Rust mà bằng F*, chính xác hơn là Low*, một DSL cấp thấp được tích hợp trong F*, và đã được xác minh hoàn toàn
https://project-everest.github.io/
https://mitls.org/
Vấn đề khi áp dụng những công cụ như vậy để xác minh một ngôn ngữ bên ngoài như Rust là phần chứng minh không được viết bằng ngôn ngữ đích, nên lập trình viên phải học cả hai ngôn ngữ. Dựa trên kinh nghiệm viết Creusot, công việc với Verus và Aeneas, cùng kinh nghiệm tại phòng nghiên cứu Why3, tôi đã suy nghĩ về việc một “Rust có ý thức về xác minh” sẽ trông như thế nào. Nếu xây dựng một ngôn ngữ như vậy ngay từ đầu, khả năng dễ xác minh có thể được cải thiện từng bước so với cả Rust, và có lẽ đặc biệt hiệu quả ở những phần khó của chứng minh
Thứ tôi thấy thiếu nhất trong chức năng mặc định là một tính năng tương đương với “hãy chạy quickcheck trên chứng minh của tôi”. Khi có code và đang cố chứng minh một thuộc tính không đúng, rất dễ vò đầu bứt tai vì không hiểu tại sao không chứng minh được. Nếu trong lúc chứng minh đi tới một trạng thái vô lý, sẽ rất hay nếu có một lệnh kiểu “hãy tạo phản ví dụ tại đây” và nó trả ra phản ví dụ. Chứng minh phụ thuộc đường đi rất mạnh và nói chung không dễ, nhưng các công cụ này có vẻ đã rất gần với sự vĩ đại. Quá trình cố chứng minh code cũng cần phản ánh khả năng rằng chính code đó có thể có bug
Prover sẽ không suy ra một chứng minh sai, mà chỉ thất bại trong việc suy ra một chứng minh hợp lệ. Tôi nghĩ không có nhiều ứng dụng machine learning có tính chất như vậy
Thực ra trong Rust, lock và reference count là các cấu trúc runtime.
Arcphá vỡ khá mạnh mô hình RAII của Rust, đến mức phải loại bỏ scoped thread, vốn yêu cầu destructor được chạy trước khi scope kết thúc. Reference count toàn cục có vấn đề về chu trình và rò rỉ, rồi lại trở thành một vấn đề mang tính toàn cục. Có lẽ khó loại bỏ hoàn toàn, nhưng tôi tin rằng tốt hơn là nhốt nó trong các scope kiểu arena. Với lock, có vẻ cần các cấu trúc dữ liệu bất đối xứng như channel. Trong Go, channel được tách thành bên gửi và bên nhận, và trong goroutine gửi có thể đặtdefer close(ch); ngay cả khi panic, nó vẫn được đảm bảo chạy sau khi phần còn lại của thread kết thúc. Không nhất thiết phải là channel, nhưng nếu tách vai trò đọc-ghi/sản xuất-tiêu thụ thì việc suy luận sẽ dễ hơn nhiều và cũng có ích cho phân tích hình thứcTôi thích việc mạch bài bắt đầu từ trích dẫn bài báo khoảng năm 1973 của Hoare và giờ đã kéo dài tới bài thứ hai. Ban đầu tôi đã viết một bình luận dài trong luồng HN về bài của boat, nói rằng việc nghiêng trích dẫn đó sang góc nhìn lấy Rust làm trung tâm là dễ hiểu xét theo nền tảng của boat, nhưng lại thu hẹp phạm vi phê phán của Hoare một cách khiên cưỡng
Giờ Grayson đã lấy mảnh hẹp đó làm điểm xuất phát để bàn về vài vùng và điểm thiết kế thú vị của Rust. Tôi vẫn nghĩ bình luận của mình là đúng, nhưng cuộc thảo luận tiếp nối từ bài của Grayson đã đủ để bù lại những bất mãn kỹ thuật của tôi với bài viết đóng vai trò điểm xuất phát
Sau đó, khi các kỹ thuật không đảm bảo tính đúng đắn nhưng tiến xa hơn kiểm thử đơn giản xuất hiện, tôi cho rằng các phương pháp không đảm bảo tính đúng đắn đã vượt lên trước các phương pháp đảm bảo tính đúng đắn
Ông đã tìm ra vấn đề, và nhìn lại thì lời giải ép buộc chia sẻ XOR khả biến bằng hệ thống kiểu trông như chỉ còn một bước nhỏ. Nếu khi đó người ta nhận ra bước nhỏ ấy chính là lời giải, có lẽ đã giảm được 50 năm đau đớn khổng lồ
Nhưng bản thân trích dẫn không có vẻ củng cố góc nhìn đó. Có thể xem đây là một nỗ lực lấy lời than phiền mang tính tổng quát hơn của Hoare về chính sự tồn tại về mặt ngữ nghĩa của tham chiếu, rồi áp vào mô hình trạng thái khả biến không có bí danh của Rust để né vấn đề. Tuy nhiên, điều này gần với việc chỉ sửa một mảnh hẹp của vấn đề lớn hơn rồi nói rằng toàn bộ vấn đề đã biến mất. Những phần bị bỏ qua, đặc biệt là phần mở đầu mục “Variables” và ví dụ ALGOL 68, nghiêng mạnh hơn nhiều về phía rằng Hoare phê phán không chỉ trạng thái khả biến mà là chính khái niệm ngữ nghĩa về tham chiếu. Tôi công nhận Rust là một nỗ lực thuần hóa một phần vấn đề, nhưng không cho rằng bất kỳ ngôn ngữ nào đã “sửa xong” vấn đề này
Tôi không rõ vì sao bài này lại được khen nhiều đến vậy. Cảm giác như nhiều lĩnh vực phân tích chương trình bị gói gọn trong một đoạn văn. Tôi thích Graydon và tôn trọng quan điểm của ông, nhưng đoạn này đã đơn giản hóa quá mức
Cách giải thích rằng các ngôn ngữ có GC không mấy khi trang bị hỗ trợ suy luận cục bộ mạnh là một lập luận người rơm. Đã có những ngôn ngữ như Pony vừa đặt vùng vào hệ thống kiểu vừa dùng GC. Ngoài ra còn có cả các lĩnh vực phân tích con trỏ và phân tích thoát, vốn suy luận tính duy nhất và xác định liệu hai tham chiếu có thể là bí danh của nhau hay không. Cốt lõi của kiểu tĩnh cũng là chia heap thành các phần không phải bí danh của nhau bằng các kỹ thuật như lớp và trường. Đây không phải chuyện JavaScript, và không nên giả vờ rằng Java/C#/Scala cùng vô số ngôn ngữ GC khác không có suy luận cục bộ về trạng thái khả biến
Lớp và trường không cung cấp suy luận cục bộ hoàn chỉnh về trạng thái khả biến. Lý do là lớp/đối tượng A có thể trở nên phụ thuộc vào trạng thái khả biến của lớp/đối tượng B. Kế thừa lớp kiểu Java tự nó bổ sung thêm nhiều độ phức tạp khi chương trình tiến hóa theo thời gian
Tất nhiên có phản ví dụ, nhưng nhìn vào các ngôn ngữ đa dụng có GC phổ biến như Java, C#, Python thì nhận định đó đúng. Có thể diễn giải rằng ý tưởng ban đầu của hướng đối tượng gần với mô hình actor ngày nay, và chỉ muốn thay đổi các cấu trúc dữ liệu được sở hữu thông qua truyền thông điệp. Nhưng các triển khai hướng đối tượng trong thực tế gần như không tiến sát mục tiêu đó. Java không ngăn việc lưu nhiều tham chiếu khả biến tới cùng một đối tượng trong nhiều đối tượng khác nhau. Bài này giải thích điểm đó tốt hơn: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Chỉnh sửa: tôi đã đọc nhầm phủ định kép. Đọc lại vẫn thấy rối. Ý là Java có suy luận cục bộ, khác với JavaScript, phải không?
Tôi thường thích các bài viết của Graydon, nhưng bài này, giống như nhiều bài viết về các kỹ thuật hình thức, có thể khiến độc giả không biết lĩnh vực này hiểu lầm. Nó giống như nói rằng phương pháp biến chì thành vàng đã được cải thiện ở mức một chữ số bậc độ lớn, nhưng lại không nói rằng để đạt hiệu quả chi phí thực dụng vẫn còn thiếu 29 chữ số bậc độ lớn nữa
Việc không có alias có làm cho kiểm chứng hình thức dễ hơn đáng kể không? Đúng. Nhưng điều đó có nghĩa là ta có thể kiểm chứng các chương trình thực tế một cách thực dụng và hiệu quả về chi phí không? Hoàn toàn không. Có những chương trình, mạch và thành phần được kiểm chứng hình thức hằng ngày, nhưng chúng là ngoại lệ, tương đối rất nhỏ, và được tạo ra theo cách đặc biệt cẩn trọng. Các thuộc tính giúp suy luận cục bộ là quan trọng, nhưng chúng không tạo ra thay đổi thực chất nào trong cách bảo đảm tính đúng đắn của phần mềm chủ đạo theo một phương pháp sound
Ngay cả các chương trình trong một ngôn ngữ rất xa với tính Turing-complete — không có heap, không có con trỏ, không có số nguyên, chỉ có biến boolean và vòng lặp không thể chạy quá hai lần — cũng không thể kiểm chứng một cách thực dụng vì chúng quy về TQBF. Với một số thuộc tính, chẳng hạn an toàn bộ nhớ, thì có thể, nhưng như vậy không đủ cho những gì phần mềm cần. Trong thập niên 1970–1990 từng có hy vọng rằng dù độ phức tạp trường hợp xấu nhất là khó xử lý, các bảo đảm cục bộ và cấu trúc của ngôn ngữ sẽ giúp tránh được trường hợp xấu nhất; nhưng về sau điều đó đã được chứng minh là không đúng. Hy vọng rằng các chương trình con người thực sự viết đủ xa khỏi trường hợp xấu nhất để có thể có heuristic tốt dường như giờ cũng không còn đúng nữa
Có một bài thuyết trình liên quan đến nội dung này: https://pron.github.io/posts/correctness-and-complexity
Kết quả cốt lõi là phần lớn các thuộc tính thú vị mà ta muốn kiểm chứng không hợp thành. Ngay cả khi chứng minh được thuộc tính cho từng thành phần P1...Pn, chi phí để chứng minh thuộc tính đó cho P1 ○ ... ○ Pn không chỉ tăng siêu đa thức theo n, mà còn tăng siêu đa thức theo kích thước của từng thành phần. Nói cách khác, nó khó như khi không chia nhỏ, và tính đúng đắn không phân rã được. Vì vậy “có thể kiểm chứng khá nhiều thứ” và “những gì kiểm chứng được chỉ là một giọt nước trong đại dương” đồng thời đều đúng, và khoảng cách này thường bị bỏ qua trong các cuộc thảo luận về kỹ thuật hình thức
Nó không hoàn toàn sai, nhưng cũng không hoàn toàn đúng. Thật đáng ngạc nhiên là dù rất nhiều người quan tâm đến chủ đề này đã có nhiều cơ hội qua hàng trăm lần lặp lại để chỉ ra điều đó, lập trường vẫn không hề tiến hóa. Thái độ như vậy nghe như một sự khép kín bệnh lý, và khiến mọi người tham gia đối thoại lãng phí thời gian
Chuyện như vậy lặp lại nhiều lần. Ngay cả khi các phương pháp sound có những cải tiến quan trọng, các phương pháp không sound trong thực tế vẫn đạt tiến bộ lớn hơn nhiều hướng tới phần mềm đúng đắn hơn. Một ví dụ rất gần đây là https://antithesis.com. Tất nhiên, trong một số bối cảnh cụ thể, các kỹ thuật sound có thể mạnh mẽ và thực dụng hơn, nên đây là một chủ đề phức tạp
unsafeđúng hay không là hợp lý. Chỉ riêng điều đó thôi cũng thật sự hữu íchTôi cũng vừa để lại một bình luận liên quan trong bài viết về F*. Chỉ xét cú pháp thì về mặt chủ quan tôi thích F*/F# hơn Rust, nhưng với phần mềm điều khiển show đang phát triển, tôi đã quyết định dùng Ada/SPARK2014
Nếu Rust muốn thu hút những người giống như Ada/SPARK2014, nó cần một tiêu chuẩn được xuất bản chính thức như các ngôn ngữ lâu đời như C, Common Lisp, Prolog, Fortran, COBOL. Rust cũng đang bước vào lĩnh vực này khi AdaCore và Ferrous Systems hợp tác để cung cấp các công cụ kiểm chứng hình thức cho Rust tương tự Ada/SPARK2014, nhưng hiện vẫn chưa có tiêu chuẩn đã xuất bản, và di sản của Ada cùng SPARK2014 là rất lớn
Thật thú vị khi có thể xem reference counting như một dạng GC tối ưu hóa chạy tức thì, hoạt động khi dùng nghiêm ngặt cho dữ liệu không có chu trình hoặc khi có thể chấp nhận rò rỉ do chu trình. Python dùng cách kết hợp reference counting + tracing như bài viết mô tả, và tôi từng thấy các triển khai vận hành ép bộ thu gom tracing chỉ chạy một lần sau mỗi N request
Perl dùng reference counting thuần túy nhưng có weak reference, nên với cái giá là phải để ý giữ reference ở phần nào trong cấu trúc chu trình, có thể biến dữ liệu thành không có chu trình theo góc nhìn reference counting. Koka về lý thuyết dùng reference counting nhưng trên thực tế cố gắng đẩy càng nhiều càng tốt sang thời điểm biên dịch; nếu bảo đảm được rằng trong
y = x + 1,xchỉ có một reference và sau đó không còn được dùng, thì có thể tái sử dụng cùng vùng lưu trữ choyđể sửa đổi tại chỗNim cung cấp ORC, tức reference counting tự động cộng với một triển khai thuật toán Recycler của Bacon+Rajan. Thuật toán này được thiết kế để chỉ thu gom các chu trình trong hệ thống dựa trên reference counting, nên khá nhanh. Quay lại phía Rust, có một triển khai Recycler stop-the-world ở đây: https://github.com/fitzgen/bacon-rajan-cc và fork này được phát hành dưới dạng crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc Mục Alternative trong README có liên kết tới các thử nghiệm khác cùng lĩnh vực. Nếu khó tìm bài báo Recycler, tôi đã gom các bản sao dưới https://trout.me.uk/gc/, và nếu cùng gu thì có lẽ bạn cũng sẽ thích các bài báo dưới https://trout.me.uk/lisp/
Tôi cảm thấy sốt ruột với kiểm chứng hình thức chương trình. Việc chứng minh một chương trình triển khai đúng đặc tả thì về mặt lý thuyết rất thú vị, nhưng giá trị thực dụng không lớn
Viết một đặc tả đúng cũng khó như lập trình đúng, nên vấn đề khó không được giải quyết mà chỉ bị chuyển chỗ. Các phương pháp hình thức có những ứng dụng thực tế, nhưng hiếm gặp
Một khi làm được việc đó, có thể ép nó thành tiền điều kiện. Ví dụ trước khi truyền một mảng vào một hàm nào đó, phải chứng minh mảng ấy đã được sắp xếp sẵn
Được viết vào ngày 15/05/2024, cũng là kỷ niệm 9 năm Rust 1.0
Tôi đã đọc bài viết được liên kết của Boats và thấy rất hay. Thật ngạc nhiên là trích dẫn của Hoare từ 50 năm trước vẫn còn liên quan, và cách diễn đạt cũng rất xuất sắc
Sẽ tốt hơn nếu có thể dùng thứ gì đó đơn giản hơn, như type guard ở thời điểm biên dịch. Khi trait bound sinh sôi, chương trình ở cấp kiểu trở nên khó đọc
Ví dụ như
Where <<::Output as G>::Output as H>::Output: HList + Zhaytype Output = <<::Output as G>::Output as H>::Output;. Rồi thêmCons>>>vào đó, và nhận ra các con số nhưU8của TypeNum tự thân cũng là các lớpCons>>lồng nhau. Có thể tạo ra tiến bộ trong lĩnh vực này và khiến nó thực hiện được các kiểm chứng mong muốn, nhưng thông báo lỗi có thể khác rất xa cách lập trình viên con người viết mã, còn triển khai thì cực kỳ đau đớnLý do trải nghiệm lập trình viên đáng kinh ngạc là vì đây không phải “chỉ là hàm”, mà là tổ hợp của các generic cụ thể và associated type. Tôi muốn dùng kiểm tra kiểu runtime nhưng chạy ở thời điểm biên dịch; tuy nhiên để làm vậy thì phải viết mã khá khác. Rốt cuộc, làm cho Rust ở cấp kiểu/thời điểm biên dịch đơn giản hơn, mang tính hàm hơn và dễ đọc hơn có thể là con đường để các dự án phân tích hình thức kiểu này đem lại trải nghiệm tốt cho maintainer và người dùng. Tóm lại là tôi muốn
comptimeRust. Và tôi cũng thắc mắc liệuFuturedựa trênPin<&mut Self>đã quá cố định rồi hay chưa. Tôi muốn thử nghiệm các triển khai nội bộ khác củaasync/await, nhưng không biết nên bắt đầu từ đâu