Phương pháp hình thức: Chỉ là thực hành kỹ thuật tốt thôi sao? (2024)

 (brooker.co.za)
1 điểm bởi GN⁺ 2025-01-12 | 1 bình luận | Chia sẻ qua WhatsApp
  • Với các hệ thống cấp thấp quy mô lớn, phân tán và quan trọng, phương pháp hình thức nên được xem là một thực hành kỹ thuật giúp giảm thời gian và chi phí, chứ không chỉ là một bước bổ sung chỉ để đảm bảo tính đúng đắn
  • Trong phần mềm, thiết kế và triển khai dễ bị trộn lẫn với nhau, nên việc sửa thiết kế muộn sẽ nhanh chóng dẫn đến làm lại phần triển khai và chi phí thay đổi API
  • Nếu xem xét cụ thể hành vi và giao diện trước khi triển khai, có thể giảm mật độ lỗi và các vấn đề sau khi đưa vào production, đồng thời đi tới thiết kế đúng nhanh hơn
  • Ở những lĩnh vực mà yêu cầu người dùng thay đổi nhanh hoặc khó hình thức hóa như UI, tài liệu hay logic giá, hiệu quả của thiết kế hình thức toàn diện trước khi triển khai có thể thấp hơn
  • Các công cụ như TLA+, P cũng có thể được dùng ở giai đoạn thiết kế để xem xét tối ưu hóa và ràng buộc, từ đó giảm đánh đổi giữa tính đúng đắn và hiệu năng

Phương pháp hình thức như một thực hành kỹ thuật tốt

  • Phương pháp hình thức là một phần quan trọng của thực hành kỹ nghệ phần mềm tốt
  • Đặc biệt có giá trị với các kỹ sư làm việc với hệ thống quy mô lớn, hệ thống phân tán và các hệ thống cấp thấp quan trọng
  • Xuất phát từ tiền đề rằng kỹ thuật rốt cuộc là hoạt động tối ưu hóa thời gian và chi phí
    • Đồng thời cũng cân nhắc hiệu năng, khả năng mở rộng, tính bền vững và hiệu quả
  • Phương pháp hình thức không rẻ, không dễ, và cũng không phải lúc nào cũng phù hợp với mọi cách phát triển, nhưng trực giác rằng nó chỉ làm tăng chi phí thì không phải lúc nào cũng đúng

Hai con đường để giảm chi phí

  • Con đường thứ nhất là giảm làm lại
    • Không giống nhiều lĩnh vực kỹ thuật khác, trong phần mềm việc thiết kế và xây dựng rất dễ diễn ra đồng thời
    • Có thể bắt đầu triển khai ngay cả khi thiết kế chưa đủ hoàn chỉnh
    • Tính linh hoạt này là điểm mạnh của phần mềm, nhưng cũng có thể biến các vòng lặp thiết kế thành các vòng lặp triển khai và làm tăng chi phí
  • Con đường thứ hai là quản lý chi phí thay đổi
    • Khi API hay hệ thống đã có khách hàng sử dụng, thay đổi sẽ trở nên đắt đỏ và khó khăn hơn rất nhiều
    • Theo Hyrum’s Law, khi một API có đủ số lượng người dùng, sẽ luôn có ai đó phụ thuộc vào mọi hành vi quan sát được, bất kể hợp đồng quy định thế nào
  • Việc cô lập hành vi hệ thống thông qua API là một ý tưởng quan trọng của kỹ nghệ phần mềm, nhưng vẫn còn giới hạn là người dùng có thể phụ thuộc cả vào chi tiết triển khai
  • Có thể triển khai lại hoàn toàn hệ thống phía sau API, nhưng sự trừu tượng hóa không làm biến mất chính chi phí thay đổi
  • Công việc thiết kế hình thức có thể giảm chi phí làm lại và xử lý thay đổi giao diện sớm hơn, từ đó tăng tốc độ và hiệu quả xây dựng phần mềm

Những hệ thống phù hợp với thiết kế hình thức

  • Không phải mọi phần mềm đều áp dụng theo cùng một cách
  • Với phần mềm có nhiều yêu cầu người dùng thay đổi nhanh hoặc khó hình thức hóa, giá trị của thiết kế trước có thể giảm đi
    • UI, website, triển khai logic giá là những ví dụ thuộc nhóm này
    • Ở các lĩnh vực này, việc làm lại liên tục có thể khiến chi phí thiết kế trước trở nên cao hơn
  • Ý tưởng nền tảng của agile là tiến hành triển khai và thu thập yêu cầu song song để rút ngắn thời gian ra mắt
    • Cho phép hoàn thành việc triển khai ngay cả khi quá trình thu thập yêu cầu vẫn đang tiếp diễn
    • Trong nhiều trường hợp, cách phát triển song song này là tối ưu hoặc là điều kiện cần để có thể tiếp tục
  • Ngược lại, nhiều phần của các hệ thống quy mô lớn, phân tán, cấp thấp lại có yêu cầu đã được hiểu rõ
    • Ít nhất là tồn tại một phần yêu cầu tĩnh đủ lớn
    • Trong trường hợp đó, thiết kế hình thức trước có thể giảm đáng kể việc làm lại và mật độ lỗi ở giai đoạn triển khai cũng như sau khi đưa vào production
  • Yêu cầu càng gần với quy luật vật lý thì giá trị của thiết kế và thiết kế hình thức càng cao; càng gần với ý kiến người dùng thì giá trị đó càng thấp

Giới hạn của việc tài liệu hóa và hình thức hóa yêu cầu

  • Việc viết rõ yêu cầu người dùng, dù theo cách hình thức hay phi hình thức, đều rất có giá trị
  • Nếu không ghi lại yêu cầu, thời gian sẽ bị lãng phí và mọi người có thể đi theo các hướng khác nhau, gây ra ma sát
  • Việc đặc tả hình thức mọi yêu cầu của con người có thể khó hoặc không kinh tế
    • Yêu cầu thẩm mỹ của UI
    • Tính dễ đọc của tài liệu
    • Tính nhất quán trong tên API
  • Sự khác biệt quan điểm về cách tiếp cận hình thức cũng xuất phát từ những cách hiểu khác nhau về việc nó là gì và có giá trị theo cách nào
  • Những cách như UML, tức chuyển mã thành các sơ đồ đồ sộ, có thể ít giá trị nếu không trực tiếp xử lý các câu hỏi khó
    • Nếu được thực hiện bằng cách làm tệ hoặc công cụ tệ, ngay cả công việc có giá trị cũng có thể trở nên vô dụng

Các phương pháp và công cụ hình thức hữu ích trong thực tế

  • Phương pháp hình thức và suy luận tự động là một lĩnh vực rộng với nhiều công cụ khác nhau
  • Bộ công cụ từng hữu ích trong lĩnh vực hệ thống cloud quy mô lớn gồm có
    • Ngôn ngữ đặc tả như P, TLA+, Alloy và các model checker liên quan
    • Công cụ mô phỏng quyết định như turmoil
      • Được dùng cùng fuzzing để khám phá không gian trạng thái một cách có hệ thống thông qua kiểm thử
    • Ngôn ngữ lập trình thân thiện với kiểm chứng như Dafny và công cụ kiểm chứng mã như Kani
    • Các kỹ thuật mô phỏng số
    • Những cách tiếp cận gần với hình thức như vẽ bảng quyết định, bảng chân trị, máy trạng thái tường minh trên bảng trắng hoặc trong tài liệu thiết kế
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 là một điểm khởi đầu để tìm hiểu các phương pháp hình thức hạng nhẹ
  • Kiểm chứng triển khai không phải là mục tiêu duy nhất
    • Các công cụ như TLA+ và P có giá trị lớn trong việc xem xét thiết kế nhanh hơn và cụ thể hơn trước khi triển khai

Xây phần mềm nhanh hơn và cũng nhanh hơn về hiệu năng

  • Khi viết How Amazon Web Services Uses Formal Methods vào năm 2015, trọng tâm chủ yếu là tính đúng đắn
    • Kiểm chứng các thuộc tính an toàn và sống của thiết kế
    • Đi tới thiết kế đúng nhanh hơn
  • Trong trường hợp của một nhóm dùng TLA+ cho hệ thống quản lý khóa nội bộ, điểm quan trọng là họ đã “kiểm chứng các tối ưu hóa táo bạo”
  • Những công cụ như TLA+ không chỉ giúp xây dựng hệ thống nhanh hơn mà còn có thể giúp xây dựng các hệ thống nhanh hơn về hiệu năng
    • Nhanh chóng khám phá các tối ưu hóa khả thi
    • Tìm ra những ràng buộc thực sự quan trọng
    • Xác nhận xem tối ưu hóa được đề xuất có đúng hay không
  • Trong nhiều trường hợp, phương pháp hình thức giúp giảm các đánh đổi khó khăn giữa tính đúng đắn và hiệu năng mà hệ thống thường dễ rơi vào

Giá trị của công cụ dùng ở giai đoạn thiết kế

  • Việc sử dụng các công cụ giúp suy nghĩ về thiết kế hệ thống ở giai đoạn thiết kế có thể tăng mạnh tốc độ phát triển phần mềm
  • Giúp giảm rủi ro và cho phép tạo ra những hệ thống được tối ưu tốt hơn ngay từ đầu
  • Với các kỹ sư xây dựng hệ thống quy mô lớn và phức tạp, phương pháp hình thức là một phần của thực hành kỹ thuật tốt

Bài viết liên quan

1 bình luận

 
GN⁺ 2025-01-12
Các ý kiến trên Hacker News

  • Xác minh hình thức phần mềm, như bài viết cũng thừa nhận, phụ thuộc rất nhiều vào loại phần mềm và quy trình phát triển
    Muốn dùng xác minh hình thức thì phải có yêu cầu hình thức về hành vi của phần mềm, nhưng phần lớn dự án và triết lý thiết kế không phù hợp với điều này. Nếu phát triển và thiết kế diễn ra cùng lúc trong khi còn chưa chắc mình muốn gì, thì rất khó áp dụng các phương pháp hình thức. Tuy nhiên, những lĩnh vực dựa vào đặc tả trước, như các hệ thống nhỏ và quan trọng về an toàn, có thể hưởng lợi lớn; phần mềm hàng không vũ trụ là ví dụ tiêu biểu

    • Tôi không thấy nó ngách đến mức đó. Chi phí mà mọi người nói đến đã giảm rất nhiều trong vài thập kỷ qua, và tôi từng dạy các công cụ như TLA+ hay Alloy cho lập trình viên chỉ trong chưa đến một tuần
      Ngày nay đây không còn là kỹ năng phải có bằng tiến sĩ hay nhiều năm nghiên cứu mới học được; việc viết các đặc tả cấp cao cơ bản cũng vậy. Dùng model checker sẽ giúp bạn học được điều gì đó về hệ thống mình đang mô hình hóa, và chỉ dùng nó cho tài liệu hóa hay đào tạo thôi cũng đã hữu ích. Sức mạnh căn bản của các phương pháp hình thức là chúng buộc bạn phải suy nghĩ đến cùng. Nhiều lập trình viên tin rằng họ có thể triển khai thuật toán đồng thời chỉ bằng đầu óc của mình, trình kiểm tra kiểu và một ít unit test, nhưng sau khi chạy model checker rồi phát hiện lỗi trong thiết kế và các giả định, họ buộc phải khiêm tốn hơn. Có rất nhiều hệ phân tán nhỏ hơn ta tưởng, và không gian trạng thái thường lớn hơn dự đoán rất nhiều trước khi ta thử hình thức hóa nó
    • Không phải tất cả hoặc không gì cả. Tôi làm với một backend rất hướng sản phẩm chưa được đặc tả hoàn toàn, nhưng một số phần trong đó đã được đặc tả hình thức
      Ví dụ, chúng tôi gắn kiểm thử dựa trên thuộc tính cho một máy trạng thái rất khó nhằn, để đảm bảo rằng dù endpoint bị gọi với đầu vào kỳ lạ nào thì máy trạng thái nội bộ cũng không thực hiện chuyển trạng thái không hợp lệ. Điều này khả thi vì phần mã xung quanh không có đặc tả hình thức, nhưng máy trạng thái thì có; nhờ vậy chúng tôi cũng tìm được những lỗi tinh vi mà unit test truyền thống chắc chắn không bao giờ bắt được
    • “Hình thức” nghĩa là “được viết bằng ngôn ngữ mà máy tính có thể diễn giải”, và đó chính là việc lập trình viên làm. Viết mã là viết đặc tả hình thức cho hành vi của chương trình, và theo định nghĩa thì mọi phần mềm đều phải làm như vậy
      Tuy nhiên, để hưởng lợi từ các phương pháp hình thức, bạn phải so sánh hành vi của chương trình với một thứ khác không phải chính chương trình, và thứ khác đó cũng phải được viết bằng một ngôn ngữ hình thức. Bạn cần hiểu chính xác hành vi mong muốn, nhưng không nhất thiết phải bao phủ toàn bộ hành vi của phần mềm. Unit test tự động cũng là đặc tả hình thức, và việc chạy chúng là một phương pháp xác minh hình thức. Chúng chỉ là đặc tả yếu hơn và xác minh yếu hơn so với thứ thường được gọi là phương pháp hình thức; về mặt khái niệm hay thực tiễn không có khác biệt định tính rõ ràng. Nếu phần mềm có thể áp dụng kiểm thử, thì rất có khả năng cũng có thể áp dụng các phương pháp đặc tả hình thức phong phú hơn, và hiệu quả so với chi phí sẽ được học qua thử-sai giống như học kiểm thử
    • Dù muốn hay không, yêu cầu rồi cũng sẽ xuất hiện. Khác biệt chỉ là bạn phát hiện chúng ở giai đoạn kỹ nghệ yêu cầu, xác minh bằng một tài liệu văn bản đơn giản và xử lý xung đột; hay vừa viết mã vừa làm sai rồi mới biết; hoặc để khách hàng phát hiện trong “sprint review”
      Rốt cuộc đây là vấn đề bạn sẵn sàng tốn thêm bao nhiêu tiền và thời gian để được gọi là “agile”. Nghịch lý là trong ba cách, giai đoạn yêu cầu truyền thống lại rẻ nhất, và cũng phù hợp nhất với tinh thần agile ban đầu, vì nó nhanh chóng hội tụ với khách hàng ở thời điểm chi phí thay đổi thấp nhất: chỉ cần sửa một dòng văn bản
    • Trọng tâm có vẻ gần với khả năng hình thức hóa hơn là thiết kế trước. Ví dụ, một hệ thống tự động hóa yêu cầu bồi thường bảo hiểm thường không thể thiết kế ngay từ đầu vì hành vi của các công ty bảo hiểm không được nêu rõ, nhưng có thể tinh chỉnh hệ thống tự động hóa khi thu thập thông tin qua tương tác
      Dù vậy, ta vẫn có thể nhận được lợi ích từ việc kiểm tra xem có bỏ sót trường hợp nào không và trong hệ thống có mâu thuẫn nào không

  • Tôi thường thấy lập luận về phương pháp hình thức kiểu “phần mềm lớn, phức tạp và khó làm đúng, vì vậy cần phương pháp hình thức”
    Một mặt, tôi cũng mong điều đó là đúng. Vì tôi mạnh ở cách học mang tính hàn lâm nên cá nhân cũng có lợi, và trong thực tế, khi phần mềm thực sự phức tạp đến mức thất bại rồi phải mò mẫm tìm nguyên nhân thì rất bực bội. Nhưng hiếm khi thấy ai chỉ ra một cách thuyết phục rằng phương pháp hình thức giải quyết vấn đề đó như thế nào. Bài viết này khá hơn ở chỗ chỉ ra rằng phần lớn “thiết kế” hiện đại là lãng phí thời gian, nhưng lại chưa giải thích đủ vì sao TLA tốt hơn UML. Nghe như ngụ ý rằng nếu đầu tư vài tháng hoặc vài năm vào TLA thì sẽ đạt được giác ngộ, và hiểu được tính hữu ích của nó theo cách không thể giải thích cho những người chưa giác ngộ. Giải tích hay thống kê Bayes cũng có phần như vậy nên không phải là chuyện bất khả, nhưng cuối cùng ta lại quay về kiểu phán đoán của nhà quản lý dự án: “nếu nó thật sự hữu ích đến thế thì đã có nhiều người dùng hơn và lợi ích sẽ tự bộc lộ”. Nếu một thứ đã tồn tại từ lâu mà vẫn chưa được chấp nhận rộng rãi, rất có thể là có lý do

    • Tôi cho rằng UML vô dụng vì cùng một sơ đồ nhưng mỗi người hiểu một kiểu, và dù rất phức tạp nhưng không thể kiểm tra được, nên có thể tạo ra các sơ đồ UML tự mâu thuẫn hoặc vô nghĩa
      Khi gặp một vấn đề khó suy nghĩ, ta sẽ dùng một “phương pháp” nào đó. Nếu là giao thức truyền thông thì mô tả bằng máy trạng thái là tốt, và TLA phù hợp với ngách đó hơn. Gần đây không có nhiều vấn đề đủ để biện minh cho mức nỗ lực ấy, nhưng khi gặp đúng loại vấn đề đó thì giá trị là rất lớn. Ngôn ngữ chuyên biệt theo miền cũng tương tự: để tránh nhiều vấn đề, dùng framework parser tốt hơn nhiều so với tự viết parser. Hiện nay phần lớn việc làm lại đến từ thay đổi yêu cầu và từ việc khách hàng nói “không phải thế” trong khi chính họ cũng không biết thật sự mình muốn gì. Một phần là do những người đưa yêu cầu không suy nghĩ đủ về hệ quả của yêu cầu đó, nhưng lớn hơn là tri thức cần thiết để ra quyết định tốt không được tập trung đủ ở một nơi
    • Tôi nghĩ lý do phương pháp hình thức không được dùng rộng rãi là vì trong thực tế không có nhiều lĩnh vực kinh doanh cần bỏ ra rất nhiều thời gian và chi phí để nâng độ chính xác của logic miền từ 98% lên 99,99%
      Phương pháp hình thức rõ ràng là một khoản đầu tư lớn. Tuy vậy, dù nhìn chung chưa trở thành chủ đạo, một phần ý tưởng của nó đã đi vào các hệ thống kiểu hiện đại
    • Tôi chỉ từng tiếp xúc với kiểm chứng hình thức trong bối cảnh các lớp phần cứng; nó giống lập trình, nhưng hiệu quả trên chi phí thì hoàn toàn khác. Chip vật lý không dễ sửa sau khi chế tạo, và kiểu thiết kế cũng rất khác
      Ấn tượng tôi có là chỉ riêng việc tính nghiêm ngặt của bộ kiểm chứng hình thức phải kết thúc trong thời gian và bộ nhớ hợp lý cũng đã áp đặt giới hạn lên độ phức tạp của thiết kế. Có lẽ chiến thắng thật sự của việc yêu cầu kiểm chứng hình thức là sửa vấn đề “phần mềm lớn, phức tạp và khó làm đúng” bằng cách khiến việc xử lý các chương trình lớn, phức tạp trở nên phiền phức
    • Nếu muốn luộc con ếch này từ từ, thay vì dạy TLA, ta nên đánh cắp sự khôn ngoan từ đó. Hệ thống kiểu đã vay mượn rất nhiều từ Hindley-Milner, và bản thân nó là một dạng chứng minh từng phần mang tính hình thức
      Tôi muốn thấy các hậu duệ của kiểm thử dựa trên thuộc tính dùng kỹ thuật SAT hoặc TLA để nhanh chóng thu hẹp không gian đầu vào theo cách có thể lặp lại. Thông qua parsing và code coverage, chúng phải suy luận được rằng truyền 12 vào một hàm không thể đi vào nhánh khác với 11, nhưng các giá trị như -1 hoặc 2^17 < n < 2^32 thì có thể khác
    • Lập luận “nếu thật sự hữu ích thì nhiều người đã dùng hơn” không tốt trong bất kỳ lĩnh vực nào, và trong phát triển phần mềm thì còn tệ gấp đôi
      Đến nay phần lớn dự án phần mềm vẫn thất bại. Điều này không hẳn là “thất bại thị trường”, mà gần với “thất bại trong việc làm ra nó” hơn

  • Phương pháp hình thức có hai nhánh lớn. Một là phương pháp ngoại tại, tách khỏi chính mã và thường suy luận về đặc tả của mã; hai là phương pháp nội tại, đi vào trong mã và suy luận trực tiếp hơn về mã
    Về mặt lịch sử, các phương pháp nội tại như hệ thống kiểu suy luận về mã ở cấp hàm, còn các phương pháp ngoại tại như bộ kiểm tra mô hình có thể quyết định được kiểu Spin/P thì xử lý mô hình mã được mô tả bằng các hình thức luận như automata. Tôi cho rằng hiện nay là thời kỳ hoàng kim của nghiên cứu phương pháp hình thức, và so với các phương pháp nội tại được thúc đẩy bởi sự phát triển của hệ thống kiểu và các dự án như Verus, các phương pháp ngoại tại dường như ngày càng ít được ưa chuộng hơn. https://github.com/verus-lang/verus

    • Các công cụ như TLA+ hoạt động tốt vì chúng nhắm tới một ngôn ngữ đặc tả rất nhỏ
      Tôi đã thấy câu hỏi rằng điều này sẽ hoạt động thế nào với một ngôn ngữ có dấu chân lớn như Rust, nhưng chưa thấy câu trả lời hay. Tôi muốn đọc thêm về nó
    • Nếu dự án Verus được liên kết kia cũng yêu cầu viết trực tiếp đặc tả về tính đúng đắn, thì tôi không rõ sự phân biệt đó có ý nghĩa gì
      Nghe như nói rằng phương pháp nội tại được ưa chuộng vì không cần viết và duy trì một đặc tả riêng, nhưng thực tế không phải vậy

  • Phần nói về phương pháp hình thức nhẹ là tốt. Duy trì một tập các chiến lược proptest bên cạnh codebase không phải khoản đầu tư lớn hơn nhiều so với viết unit test thủ công, nhưng nhờ độ bao phủ rộng và các ca thất bại nhỏ, dễ hiểu, nó đem lại insight tốt hơn nhiều
    Trên hết, cách tiếp cận này cũng rất phù hợp với thực hành phát triển phần mềm thông thường. https://crates.io/crates/proptest

    • Dạo này người ta tạo rất nhiều unit test bằng LLM. Chúng tạo khá ổn, và ta có thể yêu cầu chúng làm kỹ hơn một chút, hoặc kiểm thử các điều kiện biên nghĩ ra được, hoặc xử lý một điều kiện cụ thể
      Tôi biết ở một mức nào đó cách viết test tốt và công sức cần bỏ vào đó, nhưng LLM có thể tạo các test tốt hơn tôi nhanh hơn nhiều. Khi làm những việc lặp lại và nhàm chán, kiên nhẫn của tôi giảm xuống, nên thậm chí LLM có khả năng ít làm qua loa hơn tôi. Nếu là kỹ sư phần mềm, ta nên có phản xạ tự động hóa những việc có cảm giác lặp lại; tài liệu hóa hiện nay cũng được tạo ra nên được làm thường xuyên hơn và sớm hơn. LLM có thể tạo ra một cuộc cách mạng nhỏ trong việc áp dụng kiểm chứng hình thức. Việc tạo đặc tả đúng đắn vừa nhàm chán, vừa có thể là nhiệm vụ tương đối dễ với LLM nếu có đủ ngữ cảnh như mã đang chạy, tài liệu và gợi ý. Nếu có thể để nó tạo đặc tả rồi mình rà soát thay vì tự viết toàn bộ, động lực làm sẽ lớn hơn nhiều. Việc dùng Rust cũng là tín hiệu rằng bạn coi trọng tính đúng đắn, và compiler của nó gần như là công cụ gần nhất để chứng minh rằng hệ thống có lẽ đúng mà không cần phương pháp hình thức. Điều đó có khả năng dễ hơn nhiều so với việc gắn thêm phương pháp hình thức vào một ngôn ngữ thậm chí không có compiler hay kiểu tường minh
    • proptest hay qcheck không phải là phương pháp hình thức mà là kiểm thử ngẫu nhiên

  • Kiểm chứng hình thức cho phần mềm vẫn còn quá khó để sử dụng sao cho đáng giá, trừ các trường hợp cực đoan. Ngược lại, kiểm chứng hình thức cho phần cứng đã đến mức không có lý do gì để không dùng
    Tôi vẫn cố học, nhưng với phần lớn hệ thống, bạn phải là chuyên gia cỡ “người tự viết compiler”. Ví dụ, tôi từng cố chứng minh một bộ mã hóa/giải mã varint; 1–2 byte thì được nhưng hơn nữa thì không. Khi nhờ trợ giúp, hóa ra là do một chi tiết nội bộ không thể nào biết được, kiểu như bên trong compiler chỉ unroll vòng lặp 5 lần. Gần đây tôi đang học Lean và khá thích, nhưng lại gặp kiểu tài liệu như: “Definitional equality includes η-equivalence…”. Không phải tôi muốn chê Lean; ngược lại, trong các lựa chọn thay thế thì tài liệu của nó có vẻ còn thuộc loại tốt

    • Không biết bạn đã thử FizzBee.io chưa. Nó dùng cú pháp giống Python và ví dụ cũng đáng xem: https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      Các phương pháp hình thức không nhất thiết phải phức tạp. Vấn đề là phần lớn các phương pháp hình thức được thiết kế như bài tập học thuật để trình diễn một chủ đề cụ thể mà giáo sư quan tâm. TLA+ cũng gần với thứ được thiết kế để viết paper hơn
    • Nghe có vẻ đáng sợ, nhưng các khái niệm đó thực ra đều rất đơn giản, và nhiều khả năng là những thứ bạn đã quen thuộc rồi

  • Trong các phương pháp hình thức nhẹ, thứ tôi thích dù không quá phổ biến là kiểm chứng trace bằng logic thời gian tuyến tính: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    Về cơ bản chỉ cần log các event, và trong kiến trúc hướng sự kiện thì gần như có thể có miễn phí. Sau đó chỉ việc chạy các predicate như Always(Locked, Implies(Eventually(Unlocked))) trên trace thực thi. Có thể áp dụng cho các trace trong quá khứ, và cũng có thể kết hợp với stress test hoặc fuzzing để khám phá không gian trạng thái. Nó đơn giản, mạnh, áp dụng rộng rãi, và không cần model, chỉ cần predicate

    • Phân biệt nhỏ thôi, nhưng cái này giống testing hơn, vì nó chỉ kiểm tra công thức trên một tập con các trace của hệ thống
      Phương pháp hình thức hàm ý một cơ sở bao quát cho hành vi hệ thống. Trong TLA hoặc các hệ thống tương tự, dù đó là máy trạng thái chứ không phải hệ thống thực, đầu ra của nó là một chứng minh rằng thuộc tính LTL/CTL/TLA đúng với mọi hành vi của hệ thống, tức là mọi trace hoặc cây trace

  • Thảo luận trước đó diễn ra vào tháng 6 năm 2024: https://news.ycombinator.com/item?id=40753989

  • Quá chậm. Kế hoạch chẳng mấy chốc sẽ hóa thạch, và bất kỳ tài liệu nào cũng có thể bị dùng làm bằng chứng bất lợi tại tòa án agile

    • Nói theo kiểu gây tranh cãi thì nếu “agile đích thực” được tìm thấy, phương pháp hình thức sẽ là thứ hoàn toàn đối lập với nó. Vì những gì có thể chứng minh và tái lập được là báng bổ đối với các tín đồ chân chính

  • Phần lớn những gì tôi đọc về phương pháp hình thức có cảm giác như tạo khách hàng tiềm năng cho consultant
    Bản thân chuyện đó thì không sao, nhưng thật khó chịu khi họ hành xử như thể đã đạt giác ngộ nhờ phương pháp hình thức, rồi nói rằng nếu mua gói đào tạo cho nhân viên/đồng nghiệp hoặc thuê họ thì họ sẽ sửa các thói quen lập trình tệ hại, thậm chí nguy hiểm một cách vô trách nhiệm. Khi nào phương pháp hình thức thực sự tạo ra được code chất lượng cao không thể lệch khỏi đặc tả thì hãy nói tiếp

    • https://en.wikipedia.org/wiki/SPARK_(programming_language) thì sao
    • “Tạo ra code chất lượng cao không thể lệch khỏi đặc tả” thì sẽ hữu ích, nhưng có vấn đề căn bản: code quá cụ thể
      Trong đặc tả hình thức, thường người ta không chỉ định đến mức chi tiết đó mà chỉ định hành vi chung của hệ thống. Vì vậy một đặc tả thường tương ứng với nhiều chương trình khác nhau một cách tinh vi. Đây cũng là lý do code không đủ làm tài liệu: không thể biết đâu là lựa chọn có chủ ý và đâu là lựa chọn tình cờ. Code quá cụ thể để mô tả yêu cầu cấp cao. Ngược lại, hướng kiểm chứng chương trình theo đặc tả có vẻ khả thi hơn

  • Một số người ủng hộ phương pháp hình thức hiện nay xem những ai không dùng phương pháp hình thức là “lười” hoặc “ngu”, và muốn khẳng định sự vượt trội của mình vì họ “làm điều đúng đắn” hoặc “làm chủ một ngôn ngữ phức tạp”
    Tất nhiên không phải tất cả; tôi cũng biết những người tốt. Nhưng một số thực ra gần như là người chỉ có một ngón nghề. Nếu hỏi họ những hệ thống phương pháp hình thức khác mà họ đã học hoặc thử trong vài năm gần đây, họ sẽ nói là “quá bận” nên không học được cái mới. Những phương pháp hình thức dễ dùng hơn gần đây gồm FizzBee, dùng một dialect của Python nên đọc như pseudocode; Quint, có cú pháp dễ hơn; và P, với cú pháp quen thuộc với người dùng C#. Tác giả bài này cũng từng viết rằng phương pháp hình thức chỉ giải quyết một nửa vấn đề của mình: https://brooker.co.za/blog/2022/06/02/formal.html
    Nhưng vấn đề được nói đến ở đó đã được PRISM, vốn cũng không mới, giải quyết rồi. Chỉ là Brooker không chịu nhìn quanh hoặc học mà thôi