Vì sao viết phần mềm đúng đắn lại khó đến thế

Khi nói về kiểm chứng phần mềm, nhiều người tin rằng chỉ cần đủ công cụ tốt là có thể đảm bảo chương trình đúng đắn. Một bài viết mở rộng từ buổi nói chuyện tại hội nghị Curry On lại đi theo hướng ngược lại: tác giả dùng lý thuyết tính toán (computability theory) và lý thuyết độ phức tạp (complexity theory) để chỉ ra rằng chương trình và sự hiểu biết đầy đủ về chúng vốn mâu thuẫn với nhau ngay từ nền tảng.

Điều đáng chú ý là bài viết không phủ nhận giá trị của các công cụ hình thức, mà nhấn mạnh rằng tính đúng đắn luôn đi kèm một cái giá — giống như chi phí năng lượng khi giảm entropy — được quy định bởi những "định luật tự nhiên" của tính toán mà không công cụ nào có thể né tránh.

Sơ đồ minh họa quan hệ giữa chương trình và tính đúng đắn

Từ chương trình Hilbert đến định lý dừng

Câu chuyện bắt đầu khoảng một trăm năm trước, khi nhà toán học David Hilbert đề ra chương trình hình thức hóa toàn bộ toán học với ba trụ cột: tính nhất quán, tính đầy đủ và tính quyết định được — tức thuật toán xác định mọi phát biểu có phải định lý hay không (Entscheidungsproblem).

Năm 1930, trong bài giảng "Naturerkennen und Logik" tại Königsberg, Hilbert tuyên bố: "Chúng ta phải biết. Chúng ta sẽ biết" — câu nói được khắc trên bia mộ ông. Nhưng chỉ một ngày trước đó, Kurt Gödel đã công bố kết quả bất toàn đầu tiên, đánh sập hai trụ cột đầu tiên.

Đến năm 1936, Alonzo Church và Alan Turing độc lập chứng minh định lý dừng (halting theorem): không tồn tại thuật toán xác định liệu một chương trình bất kỳ có bao giờ kết thúc hay không. Chứng minh dựa trên phép chéo hóa (diagonalization), cùng ý tưởng Gödel đã dùng — giả sử có chương trình H quyết định dừng, ta xây dựng chương trình G phản bác lại chính H, dẫn đến mâu thuẫn.

Những hệ quả trực tiếp cho kiểm chứng

Định lý dừng kéo theo một loạt hệ quả gắn trực tiếp với bài toán kiểm chứng phần mềm:

• Bài toán khả đạt (reachability): không có chương trình nào xác định được liệu M có bao giờ đạt tới một trạng thái cho trước hay không.
• Định lý Rice: với mọi tính chất không tầm thường của hàm bộ phận, không có thuật toán nào quyết định được chương trình có thỏa tính chất đó. Ví dụ, không có thuật toán xác định đầu ra của chương trình luôn là bình phương đầu vào.
• "Định lý hải ly bận" (Busy Beaver): hàm f(n) = số bước tối đa một máy Turing có n trạng thái điều khiển có thể chạy trước khi dừng là không tính được. Với n = 6 và bảng chữ cái 2 ký hiệu, giá trị này đã lớn hơn 7,4 × 10^36534.

Điều này cho thấy việc chứng minh một chương trình dừng lại có độ khó vượt mọi hàm tính được, dù ta dùng phương pháp chứng minh động hay tĩnh.

Chương trình nhỏ, hành vi không thể chứng minh

Định lý bất toàn thứ hai của Gödel đưa ra một ví dụ ấn tượng hơn: ta có thể viết chương trình liệt kê các định lý từ hệ tiên đề ZFC và dừng khi gặp mâu thuẫn. Chương trình dừng khi và chỉ khi ZFC bất nhất — giả sử ZFC nhất quán, chương trình không bao giờ dừng, nhưng ta không thể chứng minh điều đó.

Năm 2016, Adam Yedidiya và Scott Aaronson công bố một máy Turing như vậy; Stefan O'Rear nhanh chóng cải thiện xuống còn 1919 trạng thái điều khiển. Máy này nhỏ đến mức tương đương một chương trình Python khoảng 100–200 dòng. Nghĩa là tồn tại những chương trình chỉ vài trăm dòng mà toán học về nguyên tắc không đủ mạnh để xác định hành vi của chúng.

Turing cũng nhận ra sớm điều này. Trong bài giảng năm 1947 cho Hội Toán học London, ông nói rằng khái niệm tính toán gắn với một quá trình vật lý — thuật toán là thứ được thực hiện trong thế giới thực, không phải một đối tượng toán học thuần túy.

Minh họa các tầng trừu tượng trong lập trình

Độ phức tạp: cái giá của thời gian

Tính quyết định được chưa phản ánh hết khó khăn thực tế. Năm 1952, trên sóng BBC Radio trong cuộc thảo luận công khai đầu tiên về trí tuệ nhân tạo, Max Newman hỏi Turing về yếu tố thời gian; Turing đáp rằng "yếu tố thời gian này chính là câu hỏi chứa đựng mọi khó khăn kỹ thuật thực sự".

Lý thuyết độ phức tạp ra đời năm 1965 với Hartmanis và Stearns. Bài toán dừng có giới hạn (bounded halting) hỏi: quyết định xem M có dừng trên x trong vòng n ngày bước có độ phức tạp bao nhiêu? Câu trả lời là θ(n) — không thể biết một chương trình làm gì nhanh hơn việc chạy nó. Tác giả bài viết còn đề xuất biến thể "dừng có giới hạn khấu hao" (amortized bounded halting): liệu làm việc nhiều trên một số đầu vào có giúp nhanh hơn trên tất cả đầu vào còn lại không? Câu trả lời cũng là phủ định.

Hartmanis, trong bài giảng nhận giải Turing năm 1993, coi độ phức tạp là một định luật tự nhiên tương tự các định luật vật lý — và điều quan trọng là các giới hạn tính toán này áp dụng cho cả con người (sai khác tối đa một đa thức). Theo ông, chưa từng có ví dụ nào con người vượt qua giới hạn độ phức tạp.

Kiểm chứng là bài toán khó nhất trong khoa học máy tính

Dạng tổng quát nhất của kiểm chứng: cho chương trình M và phát biểu φ trong một logic mô tả tính chất chương trình, xác định M có thỏa φ hay không — tức bài toán kiểm tra mô hình (model-checking). Bài toán này bao trùm dừng, định lý Rice, khả đạt và mọi bài toán quyết định có giới hạn trên về độ phức tạp. Nói cách khác, kiểm chứng khó hơn mọi bài toán có giới hạn tính toán đã biết.

Thu hẹp phạm vi cũng không cứu được

Có hai cách thu hẹp: giới hạn máy hoặc giới hạn tính chất. Giới hạn tính chất không giúp gì vì ngay cả những tính chất đơn giản nhất cũng bất khả quyết hoặc quá khó.

Với cách giới hạn máy, ta có thể dùng ngôn ngữ toàn phần (total language) — mọi vòng lặp có biến đếm giảm dần. Nhưng chứng minh chéo hóa vẫn áp dụng nguyên vẹn: kiểm chứng vẫn là Ω(|S|). Đáng chú ý, mọi chương trình thực tế đều có thể được xem là viết trong ngôn ngữ toàn phần bằng cách thêm bộ đếm lớn — mà không đổi ngữ nghĩa vật lý.

Một ví dụ đắt giá: chương trình Java/C khoảng 10 dòng, hoàn toàn kiểu toàn phần, không có phép toán phức tạp, sẽ "crash" khi và chỉ khi giả thuyết Goldbach sai. Các nhà toán học đã không chứng minh được chương trình không bao giờ crash suốt 270 năm. Vấn đề không phải chương trình này đặc biệt khó — mà là ta không thể nhìn vào mã nguồn để biết nó khó đến mức nào.

Tính đúng đắn không phân rã được

Với máy trạng thái hữu hạn (FSM), các bộ kiểm tra mô hình tự động đã có từ thập niên 1980 và là kỹ thuật kiểm chứng hình thức phổ biến nhất trong công nghiệp. Với logic thời gian tuyến tính (LTL), độ phức tạp kiểm tra mô hình là 2^O(|φ|) · O(|S|); với logic cây tính toán (CTL) là O(|φ||S|). Nếu coi công thức φ là hằng số, cả hai đều tuyến tính theo kích thước không gian trạng thái — chính là kết quả đã đưa Emerson, Clarke và Sifakis đến giải Turing.

Minh họa máy trạng thái hữu hạn cho giao thức truyền thông

Nhưng một kết quả năm 2005 cho thấy bài toán kiểm chứng FSM khó đến mức không thuộc lớp FPT (fixed-parameter tractable) khi tham số hóa theo số mô-đun. Nghĩa là không thể giảm công sức chứng minh tính đúng đắn bằng cách chia nhỏ thành mô-đun. Chương trình Goldbach minh họa rõ nhất: hàm bar đúng và được đặc tả tốt, nhưng ghép nó vào foo bằng một vòng lặp giảm dần và một phép trừ lại tạo ra tổng thể không thể chứng minh.

Tương tự, các trừu tượng ngôn ngữ như biến và đồng thời làm tăng độ ngắn gọn của biểu diễn lên cấp số mũ, nhưng cũng làm tăng độ phức tạp kiểm chứng đúng bằng chừng ấy. Bài toán kiểm tra mô hình tượng trưng là PSPACE-đầy đủ — tương đương việc mở rộng hoàn toàn sơ đồ trạng thái. E. Allen Emerson từng nhận xét kết quả này "có thể coi là một thực tế thực nghiệm".

Góc nhìn

Với các kỹ sư và doanh nghiệp phần mềm Việt Nam, kết luận thực dụng rút ra không phải là "bỏ cuộc với kiểm chứng hình thức", mà là nhìn đúng vào bản chất chi phí. Kiểm chứng hình thức, kiểm thử tự động hay kiểm tra kiểu mạnh đều có giá trị — nhưng chúng không thể biến một bài toán bất khả quyết thành bài toán dễ. Việc một mô-đun đã được kiểm chứng kỹ lưỡng không đảm bảo rằng hệ thống ghép từ các mô-đun đó cũng đúng, như trường hợp foo/bar cho thấy.

Hàm ý thực tế là nên đầu tư vào những gì có tỷ lệ đòn bẩy cao: thiết kế hệ thống để lỗi ít nguy hiểm hơn, giới hạn phạm vi trạng thái có thể xảy ra trong thực tế, và chấp nhận rằng luôn tồn tại phần rủi ro không thể loại bỏ hoàn toàn bằng chứng minh hình thức. Hiểu được giới hạn lý thuyết giúp đội ngũ ra quyết định đúng hơn về nơi đặt nguồn lực kiểm thử, thay vì kỳ vọng một công cụ nào đó sẽ giải quyết trọn vẹn bài toán đúng đắn.