Phương pháp hình thức và tương lai của lập trình
(blog.janestreet.com)- Phương pháp hình thức là công cụ để chứng minh phần mềm có thỏa mãn các tính chất dự định hay không, và với sự lan rộng của lập trình bằng agent, cách đánh giá chi phí·lợi ích đang thay đổi
- Jane Street trước đây cho rằng ngoài một số trường hợp đặc biệt thì phương pháp hình thức có giá trị thấp so với chi phí, nhưng nay đang lập đội ngũ chuyên trách
- seL4 đã cần 25 người-năm để kiểm chứng 8.700 dòng mã C, và mỗi dòng mã cần khoảng 23 dòng chứng minh cùng nửa người-ngày để xác minh
- Mã do agent tạo ra vẫn khác xa chất lượng có thể phát hành, vì vậy phương pháp hình thức trở nên quan trọng như một cách giảm nút thắt xác minh và cung cấp phản hồi mạnh cho agent
- Jane Street cho rằng họ có thể kiểm soát sâu ngôn ngữ và có sẵn cộng đồng lập trình viên phù hợp, nên có dư địa để cùng phát triển OxCaml với các kỹ thuật hướng chứng minh
Phương pháp hình thức và tương lai của lập trình
- Jane Street suốt 25 năm qua vẫn nói rằng ở cấp độ tổ chức họ không quan tâm tới phương pháp hình thức, nhưng giờ họ აღარ giữ lập trường đó nữa
- Họ từ lâu đã coi trọng sức mạnh của các công cụ giúp viết mã tốt hơn và đáng tin cậy hơn, và xem hệ thống kiểu là một dạng phương pháp hình thức nhẹ mang lại lợi ích lớn
- Ngoài các trường hợp đặc biệt, nhất là tổng hợp phần cứng, họ từng đánh giá phương pháp hình thức có chi phí quá cao nên không phù hợp với phần lớn phần mềm
- seL4 là một vi hạt nhân đã được kiểm chứng hình thức và là một thành tựu quan trọng, nhưng đã mất 25 người-năm để kiểm chứng 8.700 dòng mã C
- Mỗi dòng mã cần khoảng 23 dòng chứng minh, và việc xác minh một dòng cần khoảng nửa người-ngày
- Trong những trường hợp rủi ro cao và đặc tả tương đối rõ ràng như vi hạt nhân quan trọng về bảo mật, cách tiếp cận này có thể đáng giá
- Nhưng nó không phù hợp với phần lớn phần mềm, và họ cũng cảm thấy không phù hợp với cả những phần mềm quan trọng nhất của Jane Street
- Sự xuất hiện của lập trình bằng agent đã làm thay đổi đánh giá đó, khiến sự hoài nghi về tiềm năng của phương pháp hình thức chuyển thành kỳ vọng
- Jane Street đang thành lập đội phương pháp hình thức, và hy vọng biến nó thành công cụ xây dựng phần mềm hữu ích rộng rãi như các hệ thống kiểu tinh vi
Vì sao họ đổi ý
- Lập trình bằng agent đang làm rung chuyển bài toán chi phí·lợi ích truyền thống của phương pháp hình thức theo nhiều cách
- Điều đó không có nghĩa agent có thể tự mình dựng nên các chứng minh khó một cách tùy ý, nhưng mô hình vẫn giúp ích rất nhiều và cho phép nhiều người hơn sử dụng công cụ một cách hiệu quả
- Khi việc dùng phương pháp hình thức trở nên dễ hơn trước, đã đến lúc xem lại phép tính hiệu quả so với chi phí trong quá khứ
-
Nút thắt xác minh trở nên quan trọng hơn
- Mô hình ngày càng giỏi viết mã hữu ích, nhưng vẫn có khoảng cách lớn giữa mã do mô hình tạo ra và mã thực sự đủ chất lượng để phát hành
- Mô hình rất giỏi đạt được mục tiêu được giao, nhưng chưa đủ mạnh trong việc duy trì hoặc cải thiện chất lượng của codebase trong quá trình đó
- Mã do agent tạo ra đang tốt lên, nhưng vẫn có xu hướng quá phức tạp, nhiều bug lạ và trường hợp biên, đồng thời không tuân thủ các bất biến cốt lõi của codebase
- Con người phải dành nhiều thời gian để xác minh xem mã do agent tạo ra có đủ chất lượng hay không
- Phương pháp hình thức có thể giảm gánh nặng xác minh này và làm quy trình review hiệu quả hơn
-
Agent mạnh lên nhờ phản hồi
- Agent hưởng lợi từ phản hồi cả khi được huấn luyện bằng học tăng cường lẫn khi được dùng để lập trình
- Phương pháp hình thức có thể trở thành một dạng phản hồi mạnh giúp nâng cao khả năng giải các bài toán khó của agent
- Kiểm thử cũng rất có giá trị, và có thể còn tốt hơn khi kết hợp kiểm thử dựa trên thuộc tính với fuzzing
- Nhưng chỉ kiểm thử thì chưa đủ, vì nó có giới hạn nội tại trong việc bao phủ không gian trạng thái mà chương trình có thể khám phá
- Từ trải nghiệm lập trình với OxCaml, agent hưởng lợi lớn từ đảm bảo phổ quát mà hệ thống kiểu mang lại
- Nếu hệ thống kiểu có thể ngăn data race, thì có thể loại bỏ data race
- Nếu kiểu được thiết kế tốt để khiến lỗ hổng cross-site scripting trở nên bất khả thi, thì có thể loại bỏ lỗ hổng theo cách mà kiểm thử đơn thuần khó làm được
- Kiểu dữ liệu giúp giảm nút thắt xác minh và cung cấp phản hồi tốt hơn khi lập trình cùng agent
- Việc tận dụng các kỹ thuật chứng minh mạnh hơn có thể mở ra thêm dư địa cải thiện
Vì sao làm điều này ở đây
- Cả thế giới đang suy nghĩ về ý nghĩa của agent đối với tương lai của lập trình, và cũng có nhiều startup muốn kết hợp phương pháp hình thức với agent
- Jane Street có thể kiểm soát sâu ngôn ngữ mà họ sử dụng, nên có thể điều chỉnh ngôn ngữ để phù hợp hơn với các kỹ thuật hướng chứng minh
- Có nhiều hướng khả thi
- Có thể tích hợp đặc tả mô-đun của các thuộc tính vào hệ thống kiểu
- Có thể thêm các ràng buộc ở cấp kiểu cho những yếu tố như quyền sở hữu và tính khả biến để giúp một số chứng minh trở nên dễ hơn
- Có thể đưa trực tiếp các kỹ thuật chứng minh vào ngôn ngữ
-
Cộng đồng lập trình viên đã sẵn sàng
- Ở Jane Street có một cộng đồng lập trình viên sẵn sàng tiếp nhận các kỹ thuật này
- Với những người làm ngôn ngữ lập trình, việc khiến các ý tưởng tốt hơn được dùng trong công việc thực tế thường khó hơn cả việc tạo ra chính các ý tưởng đó
- Ở Jane Street, người dùng thường xuyên phàn nàn rằng các tính năng hệ thống kiểu mới lạ đã được hứa hẹn không ra mắt đủ nhanh
- Có rất nhiều người ở đây có nền tảng để tận dụng các kỹ thuật này, và mối quan tâm tới kết quả đúng đắn cùng phần mềm chất lượng cao cũng đã ăn sâu
- Một cộng đồng người dùng tích cực và kỳ vọng cao cho phép họ vừa thử các cải tiến ngắn hạn vừa theo đuổi tầm nhìn dài hạn
- Các cải tiến ngắn hạn có thể tạo tác động tương đối nhanh
- Tầm nhìn dài hạn sẽ là những mục tiêu tham vọng hơn có thể đạt tới trong vài năm
- Họ có thể học từ các thử nghiệm ngắn hạn để xây dựng hướng tới mục tiêu dài hạn
-
Quan hệ với các công cụ bên ngoài
- Họ không bỏ qua công việc của thế giới bên ngoài, và đang lấy kỳ vọng cũng như cảm hứng từ nỗ lực của nhiều cộng đồng ngôn ngữ lập trình
- Các công cụ liên quan gồm Lean, Dafny, Rocq, Agda, Iris v.v.
- Họ đang tìm cách tích hợp OxCaml với một số công cụ để tận dụng hạ tầng xuất sắc đã tồn tại
- Đồng thời họ cũng cho rằng có những lợi thế riêng chỉ có thể đạt được khi xử lý đồng thời cả ngôn ngữ lẫn kỹ thuật chứng minh
Hướng dẫn tham gia
- Jane Street đang tuyển người liên quan đến phương pháp hình thức tại London và New York
- Hiện việc phỏng vấn cho các vị trí này và xây dựng đội ngũ vẫn đang ở giai đoạn đầu
- Còn rất nhiều việc phải làm trong thời gian tới, và họ đang tìm người gia nhập đội
Bổ sung
- Khi xử lý các chứng minh phức tạp, mô hình vẫn cần sự trợ giúp và định hướng của con người
- Lập trình viên con người có thể có ý tưởng về vì sao hệ thống hoạt động và cách chứng minh nó ở mức độ cao
- Phần lớn lập trình viên không biết cách mã hóa ý tưởng chứng minh theo cách thỏa mãn một hệ thống chứng minh cụ thể
- Mô hình có thể tự động hóa nhiều công việc lặp lại trong các chi tiết kỹ thuật của việc viết chứng minh và cung cấp chuyên môn
- Những lối thoát như
Obj.magiccó thể cho phép vượt qua các ràng buộc ở cấp kiểu - Nếu theo dõi và cấm những ngoại lệ như vậy trong phần lớn mã nguồn, có thể đạt trạng thái rất gần với đảm bảo phổ quát
- Phương pháp hình thức có thể khiến lý do vì sao việc dùng các lối thoát như vậy thực sự an toàn được nêu rõ một cách tường minh
1 bình luận
Ý kiến Hacker News
Vài chục năm trước đã làm công việc chứng minh tính đúng đắn, và hệ thống khi đó thực ra có mức tự động hóa chứng minh nhiều hơn khá nhiều hệ thống về sau
Phần dễ thì do bộ đơn giản hóa Oppen-Nelson, cũng là SAT solver đầu tiên, xử lý; phần khó thì do bộ chứng minh Boyer-Moore đảm nhiệm, dùng heuristic và các bổ đề trước đó. Phần khó của con người là để bộ chứng minh thử trước rồi đề xuất các bổ đề có thể dùng cho những chứng minh sau
Các hệ thống về sau có vẻ ít tự động hóa hơn, và có cảm giác lý do phương pháp hình thức đi chệch hướng là vì quá sa vào chủ nghĩa hình thức thay vì công việc thực tế. Từ góc nhìn của người muốn có mã không lỗi cho dự án thương mại, các dự án kiểu học thuật dường như mắc thiên kiến của giới toán học, thích ký pháp ngắn gọn để viết bài báo và phân tích ít trường hợp hơn
Trên thực tế cần rất nhiều việc cày tự động và ít cần đến trực giác hơn. Những người thông minh cứ tiếp tục tạo ra các logic mới như modal logic, temporal logic để tránh sự dài dòng của chứng minh giấy bút, nhưng điều đó không giúp được bao nhiêu. Sự thật nền tảng của lĩnh vực này là phần lớn định lý khá tầm thường
Như người ở Jane Street nói, khả năng kiểm soát ngôn ngữ là một lợi thế lớn. Các mệnh đề kiểm chứng nên được tích hợp vào trong ngôn ngữ lập trình; nếu bị nhét vào chú thích, cú pháp khác, hay file riêng thì chỉ làm tăng thêm việc không cần thiết. Việc Jane Street thúc đẩy theo hướng này có vẻ rất tốt
Đã làm việc này quá sớm, hơn 40 năm trước, khi đó chỉ riêng việc xây dựng số học từ đầu bằng bộ chứng minh Boyer-Moore cũng mất khoảng 45 phút thời gian tính toán, còn bây giờ thì chưa đến 1 giây
https://archive.org/details/manualzilla-id-5928072/page/n3/m...
Logic trong khoa học máy tính và kỹ nghệ phần mềm giữ vai trò giống như giải tích trong vật lý, cơ khí và xây dựng. Những thứ như LTL hay separation logic gần đây là các đột phá cực lớn
TLA+ khá phổ biến chính là bằng chứng cho điều đó, và model checking rất thực dụng. Điều thú vị hiện nay là các phương pháp hình thức nặng hơn, đặc biệt là chứng minh định lý, có thể sớm đủ rẻ để dùng cả trong phần mềm hệ thống phổ thông
Việc viết đặc tả hình thức cho hàm, rồi tổng hợp bằng cách lai giữa SAT/SMT, bộ chứng minh định lý và LLM, sau đó nhận chứng minh tính đúng đắn, có thể sớm trở thành tiêu chuẩn
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
Điều đáng lo là sẽ xuất hiện loại toán học khó giải mã, được canh giữ bởi một nhóm tín đồ thiểu số. Các ký pháp khó hiểu khác nhau sẽ không tương thích với nhau, và hiểu được một cái cũng chưa chắc giúp ích nhiều để hiểu cái khác. Đa số rồi sẽ chỉ viết các câu tiếng Anh không thể kiểm chứng đúng nghĩa
Tệ hơn nữa, người ta có thể để máy tự hình thức hóa câu chữ của mình rồi tham gia vào màn kịch kiểm chứng mà chẳng hiểu chủ nghĩa hình thức hay chứng minh đó, để rồi khi mọi thứ nổ tung thì lại giả vờ ngạc nhiên
Hiện đang chậm rãi làm việc để tích hợp khả năng kiểu này vào những chỗ mà type system không thể xử lý nhanh, nên rất quan tâm đến góc nhìn của những người đã đi trước con đường này
Hay đấy. Trong vài tháng gần đây, đã dùng các kiểu dữ liệu có tính biểu đạt cao trong Scala 3 để chuyển dần sang việc nhét ngày càng nhiều chứng minh ở thời điểm biên dịch vào type. Không dùng macro, dù có vài cái cũng đáng dùng
Cách này không chỉ giúp giảm vấn đề agentic testing lan rộng, mà dường như còn ngăn tác tử rơi vào kiểu làm việc chất lượng thấp. Đặc biệt, nó ngăn hiện tượng tích lũy danh từ khi tác tử cứ muốn tạo kiểu tổng đơn hình mới cho mọi thứ, kể cả khi đáng ra nên khái quát hóa một cách hợp lý
Có cảm giác hướng giúp tăng tốc agent coding chất lượng cao là các công cụ mang dáng dấp của phương pháp hình thức, kể cả các ngôn ngữ có type system mạnh
Ở đây, kiểu dữ liệu có tính biểu đạt cao nghĩa là những kỹ thuật mà nếu cả nhóm chưa quen với lập trình ở cấp độ kiểu thì sẽ không muốn đưa vào codebase thông thường. Tức là đó phải là một nhóm xem higher-kinded types và type functions không phải thứ kỳ quặc mà là các khối xây dựng cơ bản
Tác tử, xét về mặt tri thức, thường “giỏi toán” hơn phần lớn lập trình viên, và nhiều khi còn tốt hơn cả những lập trình viên bị nhuộm màu bởi category theory. Hơn nữa, nếu xem nó có mức kiên nhẫn “vô hạn” trong hội thoại thì khả năng dạy học cũng khá tốt
Cá nhân thì đã nhờ Codex chuyển vài chứng minh sở thích sang kiểu Lean và thấy rất dễ. Không dám nói là đúng 100%, và để kiểm tra kỹ hơn thì cần học thêm Lean 4, nhưng về cơ bản có vẻ nó cũng kiểm tra được các bẫy chứng minh cổ điển. Rất háo hức với tương lai của phương pháp hình thức
Có vẻ như đây là câu chuyện về việc vì Gen AI tạo ra rất nhiều mã, nên giá trị của con người nên chuyển sang phía kiểm chứng. Thỉnh thoảng tôi cũng nghĩ lập trình thực sự là gì
Với người không dùng tiếng Anh là tiếng mẹ đẻ, bản thân việc học lập trình đã là một thử thách lớn. Muốn hiểu tài liệu tiếng Anh chưa được dịch thì phải dựa vào máy dịch, còn tài liệu bằng ngôn ngữ của tôi thì chậm hơn khoảng 5~6 năm
Giờ thì việc review hàng chục nghìn dòng mã do AI tạo ra là bất khả thi, nên tôi thấy xuất hiện những bàn luận về việc lập ra các quy tắc tuyệt đối như chứng minh toán học. Đọc bài này khiến tôi nghĩ đến borrow checker của Rust. Thực tế, nếu dùng Rust vài lần, nhiều người thường hình thành thói quen xấu là tìm mẹo lách để né borrow checker
Khi tính chặt chẽ toán học trở nên quá mức, con người sẽ tìm đường vòng. Những lập trình viên ít được đào tạo như tôi lại càng dễ như vậy
Tôi nghĩ những nỗ lực này rốt cuộc sẽ dẫn đến việc viết mã chỉ cho những câu trả lời đã được hình thức hóa cụ thể. Nếu chuẩn hóa theo cách đó, tôi không chắc nó có thể đáp ứng được nhu cầu của con người hay không
Những nỗ lực lập trình phòng thủ như thế này thì ổn, nhưng theo cách tôi gọi, tôi muốn làm lập trình tấn công. Tức là chấp nhận rủi ro, nhưng sửa nhanh và phát hành nhanh, tin rằng theo thời gian nó sẽ đủ tốt
Tất nhiên, trong những ngành lâu đời như Jane Street, nơi độ chính xác quan trọng và phạm vi công việc được xác định rõ, cách tiếp cận trong bài này là phù hợp. Vì có đủ dữ liệu để mô hình hóa nhu cầu của thị trường một cách thích đáng
Nhưng với một kẻ thất bại xã hội như tôi, cứ phải di chuyển liên tục để tìm mỏ vàng mà kiếm tiền, phương pháp như vậy trông giống một thứ xa xỉ. Tôi biết rõ những doanh nghiệp hiện hữu có mô hình hóa trưởng thành cần nhân lực chuyên môn trình độ cao liên tục tối ưu hóa, mà thực tế thì không thể theo kịp nhu cầu đó. Vì vậy tôi tìm những nơi mà mô hình hóa chưa được cấu trúc, nhưng ngay cả ở đó tôi cũng không biết liệu cách tiếp cận này có dùng được không
Ở đó không có chuyện “sửa là được”. Đến lúc bạn hiểu chuyện gì đã sai thì có thể đã mất hàng tỷ rồi
Vì thế cách làm tấn công có thể hiệu quả ở những lĩnh vực không cốt lõi
Tham khảo thêm thì hiện nay nhiều nơi đã dùng cách làm phòng thủ rồi. Python, Java v.v. có garbage collector, và theo nghĩa nào đó điều đó xác nhận rằng mã chạy như dự định
Tôi từng tự hỏi đến bao giờ kiểm chứng hình thức mới bắt đầu xuất hiện, nhưng việc chuyển từ giai đoạn lo chi tiết triển khai sang giai đoạn mô tả vấn đề theo cách khoa học và toán học là điều tự nhiên
Vì Gen AI, chi phí của lập trình phòng thủ đã giảm mạnh, còn chi phí kiểm chứng bởi con người thì tăng mạnh. Trong khi đó, các kỹ thuật hình thức giúp việc kiểm chứng rẻ hơn, nhưng lại có overhead triển khai lớn như phải viết đặc tả, kiểu, chứng minh và uốn phần triển khai vào một khuôn khổ cứng
Nhưng Gen AI có thể tự động hóa chính phần việc khó nhằn đó. Hai thứ này đúng là trời sinh một cặp
Sẽ cần một chút nỗ lực, nhưng loại bỏ được overhead dịch thuật liên tục thì sẽ giúp ích rất nhiều
Chỉ là tôi không rõ việc tự gọi mình là “kẻ thất bại xã hội” hay chuyện trong sự nghiệp bạn không theo các thực hành kiểu này thì liên quan gì đến luận điểm này
Gần đây tôi đang thử nghịch với các ý tưởng liên quan, và điều khiến tôi ngạc nhiên là các mô hình tiên tiến nhất, đặc biệt là ChatGPT-5.5, hoàn thành các chứng minh thủ công cụ thể trong Roqc, trình hỗ trợ chứng minh Coq trước đây, tốt đến mức nào
Các chứng minh không phải lúc nào cũng đẹp, nhưng ChatGPT thường chứng minh được trong vài phút, trong vòng 10~100 lần lặp, những việc mà tôi với kinh nghiệm trợ lý chứng minh còn hạn chế nhưng không phải bằng 0, cùng kinh nghiệm miền khá lớn về các bổ đề đang được chứng minh, sẽ phải mất lâu hơn rất nhiều
Điều khiến việc này thú vị trong bối cảnh của bài ngắn này là nó làm lung lay giả định nền tảng mà một số công cụ kỹ thuật hình thức hoạt động dựa vào. Frama-C, Ada/SPARK v.v. tập trung vào việc tạo ra các nghĩa vụ chứng minh mà những công cụ như CVC5, Z3 có thể tự động giải quyết, và nếu thất bại thì chuyển sang phương án thay thế khá đau đớn là chứng minh thủ công trong Roqc
Luồng điển hình là phát hiện ra một nghĩa vụ nào đó là “khó”, tức không thể tự động giải quyết, rồi tái cấu trúc tập hợp các bổ đề và assertion thấy được tại điểm sinh nghĩa vụ trong mã để biến nó thành thứ “dễ”, thậm chí có khi còn sửa cả mã
Điều này hợp lý trong một thế giới mà chứng minh Roqc đắt gấp đôi. Vì con người khó viết chúng, và khi mã cùng các chứng minh xung quanh thay đổi thì độ biến động bảo trì cũng rất lớn
Nhưng nếu chứng minh Roqc trở thành thứ “AI tự động giải quyết trong vòng lặp”, thì chênh lệch chi phí này biến mất. Khi đó ta có thể viết chứng minh như viết mã, ưu tiên số 1 là sự rõ ràng dễ đọc cho con người, còn tối ưu hóa cho compiler hay prover thì để rất lâu sau. Tôi vẫn chưa tiêu hóa hết các hệ quả của chuyện này, nhưng nó khá thú vị
Tôi chưa từng làm việc với chứng minh, nhưng thỉnh thoảng tôi đã thấy chuyện khi nói “sau thay đổi này test bị fail”, AI lại sửa luôn test thay vì sửa mã để vừa qua được test cũ theo đúng ý tôi vừa qua được test mới
Tôi rất mong chờ những gì sẽ đến
Mỗi khi đọc về đặc tả hình thức, tôi lại có cảm giác nó giống như “viết cùng một bài test theo cách khác”, hoặc tệ hơn là “viết cùng một phần triển khai theo cách khác”
Viết hai lần thì có thể giúp bắt lỗi, nhưng nếu đặc tả hình thức cũng có thể mang đúng những lỗi như test hay phần triển khai, thì tôi không rõ điểm đặc biệt nằm ở đâu
Vấn đề cốt lõi là để chứng minh một cách hình thức rằng chương trình làm được điều gì đó, bạn phải định nghĩa điều “gì đó” ấy một cách rất cụ thể. Khi đó trên thực tế nó lại giống như đang viết lại test hoặc phần triển khai
Tôi đã thỉnh thoảng tìm hiểu chủ đề này trong vài năm, và vẫn luôn có cảm giác mình đang bỏ lỡ điều gì đó, nhưng không biết đó là gì. Có ai giải thích giúp được không
Điểm yếu của test là bạn chỉ có thể kiểm tra những hành vi mà bạn nghĩ có thể gây vấn đề. Nếu muốn chủ động sửa cả những hành vi mà bạn còn chưa biết là có thể sai, bạn cần những công cụ khác thường hơn trong hộp đồ nghề. Fuzz testing là một khởi đầu theo hướng đó, và kiểm chứng hình thức cũng là một khởi đầu khác
Tất nhiên, chất lượng của các công cụ này phụ thuộc vào việc bạn viết được một mô hình hình thức đủ bao quát để cho phép hành vi mong muốn và cấm hành vi không mong muốn đến mức nào, và ở nhiều lĩnh vực chúng ta vẫn còn xa đáng ngạc nhiên so với điểm đó
Ví dụ, với unit test bạn có thể viết “foo('abc') trả về một chuỗi không có khoảng trắng ở cuối”
Nhưng với phương pháp hình thức, bạn có thể chứng minh rằng “với mọi đầu vào x, foo(x) trả về một chuỗi không có khoảng trắng ở cuối”
Đây là ví dụ đơn giản, nhưng cũng có thể hình dung những thứ phức tạp hơn như “với mọi chương trình P, compile(P) hoạt động giống như P”
Tất nhiên, bạn vẫn phải định nghĩa “hoạt động giống” là gì
Bạn chỉ định các thuộc tính của thiết kế, rồi công cụ sẽ kiểm tra thiết kế theo nhiều cách để xem liệu có thể vi phạm các thuộc tính đó hay không
Ví dụ, với hệ thống điều khiển đèn giao thông, bạn có thể chỉ định thuộc tính rằng các làn xe giao cắt không được đồng thời, hoặc trong một khoảng thời gian nhất định, cùng có đèn xanh
Công cụ có thể kiểm tra điều này bằng duyệt toàn bộ không gian trạng thái, và có thể hiển thị vết thực thi của đoạn mã vi phạm
Một hệ thống kiểu được chứng minh tĩnh cho phép mỗi thành phần được kiểm tra khớp với mọi thành phần khác từ trước. Không chỉ là “test này pass”, mà còn đảm bảo rằng khi ghép lại, “tất cả các test này tạo thành một tổng thể hợp lý và nhất quán”, đồng thời ngăn một mô hình không nhất quán bị triển khai thành mã
Nó hơi giống việc mở rộng yêu cầu của
matchtrong Rust — phải bao phủ đầy đủ mọi nhánh có thể — lên quy mô toàn bộ codebaseĐúng là nó không thể cứu bạn khỏi những lỗi logic hay sai lầm lý thuyết ở tầng gốc. Nhưng bạn có thể sẽ ngạc nhiên vì nó vững chắc hơn rất nhiều so với việc kết hợp hệ thống kiểu của Haskell, kiểm thử hàm ad hoc và property testing. Toàn bộ tập hợp đó vốn đã là một hệ thống mạnh, nhưng mật mã học được chứng minh hình thức còn đặt ra tiêu chuẩn cao hơn nhiều
Điều này đặc biệt có giá trị trong các tình huống đồng thời, phân tán và đa luồng. Race condition và deadlock cực kỳ khó để kiểm thử và suy luận; những câu hỏi kiểu “A, B, C có thể xảy ra theo thứ tự A, C, B không” là ví dụ điển hình
Tôi nghĩ độ trưởng thành của lĩnh vực này sẽ tiến triển đại khái như sau. Thứ nhất, LLM sẽ giúp việc học và sử dụng các phương pháp hình thức nhanh hơn rất nhiều, dù lúc đầu có thể chỉ dừng ở kiểu hậu kiểm “làm lại lần hai”
Thứ hai, sẽ chuyển sang tự động hóa nơi LLM kiểm tra kiểu “mã triển khai đã thay đổi, vậy có vẻ như nó đã phá vỡ mô hình không?” Dù vẫn chưa mang tính quyết định hoàn toàn, nó rất có thể vẫn tốt hơn nhiều so với việc bắt con người review một thứ chỉ thỉnh thoảng mới thay đổi
Thứ ba, cú nhảy thực sự sẽ nằm ở việc đưa các công cụ kiểu “chỉ viết đặc tả hình thức rồi sinh phần triển khai” lên cấp độ tiếp theo. Đã có khá nhiều dự án sinh mã như vậy, nhưng phần lớn vẫn chưa đủ chín để đạt mức mà các công ty mong muốn. Sẽ ra sao nếu công cụ LLM có thể tăng tốc 1–2 năm làm thủ công để điều chỉnh một trong số đó cho phù hợp nhu cầu
Bài viết trước của Kleppmann https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... cũng đáng đọc, và dĩ nhiên cũng nên cân nhắc xem những gì có thể đưa vào type system hay linter thì có nên làm như vậy không
Tôi hy vọng sẽ xuất hiện những cách dễ dùng hơn. Trong số các công cụ được nhắc trong bài, dafny và iris có vẻ là gần với ứng dụng công nghiệp nhất. Tôi cũng biết Amazon S3 có lịch sử dùng TLA nội bộ
Nhưng tôi vẫn chưa thấy “TypeScript của lĩnh vực này” — một thứ hòa vào công cụ hiện có một cách tự nhiên, hoạt động như zero-cost abstraction, và khiến mọi người thực sự thích hơn cách làm cũ
Ngay cả dùng linter tùy chỉnh cũng vẫn khá tệ.
golangci-lintlà một codebase đau khổ, còn semgrep thì tôi chưa dùng nhưng rule engine của nó trông khá đáng ngại. Tôi cũng chưa dùng được API AST nào mà mình thật sự thíchLời ca ngợi như thế dành cho suy luận diễn dịch, tức “phương pháp hình thức”, luôn bỏ sót giới hạn căn bản của nó: các tiên đề và định nghĩa khớp với miền đối tượng đến mức nào
Nó giống như câu “Về lý thuyết thì lý thuyết và thực tế không khác nhau. Nhưng trong thực tế thì…”. Tôi đoán Jane Street sẽ duy trì một codebase lớn nơi mục đích của mã là triển khai các thuật toán tất định nên ánh xạ là 1:1. Nhiều lập trình viên làm việc trong những lĩnh vực như vậy, nhưng hàng triệu người thì không. Phần lớn UI, phần lớn công việc mang tính thăm dò, v.v. là như vậy
Song song với phương pháp hình thức, cũng có một xu hướng cố gắng định nghĩa tiêu chí chấp thuận ở độ phân giải cao, dù không theo cách logic-toán học. Ít nhất xu hướng này vật lộn với bài toán ánh xạ, nhưng ở phần lớn nơi mà bản đồ không phải là lãnh thổ, nó không giải quyết được
Trang kết quả tìm kiếm của Google có một framework tối ưu hóa nội bộ cực kỳ tiến hóa, nhưng liệu nó đã thật sự đạt điểm tối ưu chưa? Có phải một nguyên mẫu dựng vội để nắm bắt một ý tưởng mơ hồ lại có thể cho thấy tốt hơn không? Những câu hỏi như vậy được trả lời tốt nhất khi nhìn ra bên ngoài mà hệ thống đó phục vụ, chứ không phải vào bên trong hệ thống
Mạch logic, thành phần CPU dùng nhiều formal verification, kernel, giao thức, parser, compiler, mật mã học, framework bảo mật, các nguyên thủy đồng thời, v.v. đều hưởng lợi lớn từ việc kiểm chứng
Nếu muốn tìm hiểu thêm, bài viết của Hillel Wayne là một điểm khởi đầu tốt: https://www.hillelwayne.com/formally-specifying-uis/
Và trong một số trường hợp, kể cả khi kết quả không được xác định rõ thì vẫn có thể học được, nên đây không chỉ là vấn đề ngồi xuống suy nghĩ xem điều gì sẽ hợp lý
Với tư cách là người có chút quan tâm đến thiết kế và triển khai ngôn ngữ lập trình, câu này thật sự rất thú vị với tôi. “Đối với phần lớn những người làm việc với ngôn ngữ lập trình, phần dễ là nghĩ ra những ý tưởng mới và tốt hơn để cải thiện việc lập trình. Phần khó là thuyết phục ai đó dùng ý tưởng đó cho công việc thực tế”
Hoàn toàn đồng ý. Dù có lợi ích đi nữa, vẫn có giới hạn đối với mức độ xa lạ có thể đưa vào một ngôn ngữ mới
Nhưng các tác nhân AI sẽ không cảm thấy nhiều sự kháng cự trước những ý tưởng mới mang tính cấp tiến trong thiết kế ngôn ngữ lập trình. Tôi đã nghĩ một thời gian về việc thiết kế ngôn ngữ lập trình sẽ tiến hóa thế nào sau AI dạng tác nhân
Sẽ rất thú vị khi xem ta có thể tạo ra những ý tưởng mới nào để cải thiện ngôn ngữ lập trình, khi nỗi lo về việc được chấp nhận giảm đi rất nhiều
https://steveklabnik.com/writing/the-language-strangeness-bu...
Tôi đang làm việc theo hướng áp dụng phương pháp hình thức vào kiểm thử bảo mật ứng dụng, và cho rằng có thể áp dụng cùng cách tiếp cận đó vào việc kiểm chứng business logic
Tôi đang dùng taint analysis cho việc này. Đây là một cách tiếp cận phương pháp hình thức khá vững vàng, nhưng do độ phức tạp của luồng dữ liệu trong các codebase thực tế nên ngoài hiện trường nó vẫn chưa được áp dụng rộng rãi
Việc mở rộng phương pháp hình thức vượt ra ngoài AST pattern matching và kiểm tra kiểu đơn giản là công việc thực sự khó. Phải mất nhiều năm R&D mới đạt đến mức có thể truy vết luồng dữ liệu liên thủ tục trong các codebase thực tế chỉ trong vài phút bằng taint analysis và tìm ra các lỗ hổng ẩn rất sâu
Nếu quan tâm, bạn có thể xem dự án: https://github.com/seqra/opentaint
Khoảng 18 tháng trước tôi bắt đầu mê việc dùng kiểu cùng với LLM, và trở nên nghiêm túc với
lean4vào khoảng 6–8 tháng trước. Giờ thì tôi thậm chí không cân nhắc dùng hỗ trợ AI cho công việc phần mềm nếu không có nền tảng chứng minhCICvới C/C++ FFI thực dụng, tức là trên thực tế có thể kết nối với gần như mọi thứTôi đã cấm toàn bộ từ JSON đến Python, và cũng viết lại cả
nixđể có compiler. Gần như mọi thứ chúng tôi dùng không chỉ bị property testing và nhiều dạng fuzz test hành hạ đến giới hạn, mà còn có các chứng minhlean4điều khiển property test ít nhất thông qua liên kết.olean. Khi có thời gian, chúng tôi còn chứng minh cả tính đầy đủ của toàn bộ miền và kiểm thử cả thuộc tính đóTất cả phần cần tốc độ đều được sinh từ
lean4, nên chúng tôi bỏ qua tranh luận C++/Rust. Có lợi thế khi lỗi trong C++ thực ra là lỗi trong mãlean4, nhưng có thể đi theo cả hai hướngĐây là một thay đổi lớn, và tôi không trách những người hoài nghi kiểu “Cấm JSON và Python á?”. Nhưng chúng tôi đã kiểm tra hàng triệu dòng theo cách này, và AI + hệ thống kiểu hình thức là một bước nhảy lớn hơn nhiều so với từ không có AI sang AI và Python. Theo kinh nghiệm của chúng tôi, vế sau không tiến triển đơn điệu, còn vế trước thì gần như luôn tiến triển đơn điệu
Cũng có thể làm những việc khá táo bạo. Đây là chứng minh hình thức cho phép tính tensor đa diện mà các thứ như ISL và CuTe mô hình hóa; dùng nó, ta có thể thực hiện swizzling và tiling trên thiết bị bằng
mdspancủa C++23 và còn chứng minh rằng điều đó là đúng. Tuy nhiên ví dụ này không cho thấy rõ lập luận kiểu L'Hopital về độ bao phủ: https://github.com/b7r6/mdspan-cuteKết quả thật sự rất nhanh, và nhanh ngay từ lần thử đầu tiên
https://straylight.software/assets/lambda-hierarchy.svg