Góc nhìn thực tế về Phân tích Chương trình (Program Analysis)

Khoảng mười năm trước, tôi bắt đầu nghiêm túc suy nghĩ về cách làm cho việc viết các chương trình đúng đắn trở nên dễ dàng hơn. Việc nghiên cứu câu hỏi này đã dẫn tôi đến các chủ đề như phương pháp chính thức (formal methods) và hệ thống kiểu (type systems) — những kỹ thuật giúp thiết lập rằng một chương trình nhất quán tuân theo một số quy tắc nhất định. Tuy nhiên, tôi vẫn chưa chắc chắn làm thế nào để chứng minh phần mềm thực sự đúng đắn. Không phải theo nghĩa là các lệnh được thực thi tạo ra kết quả phù hợp với đặc tả kỹ thuật, mà theo nghĩa là chương trình này thực sự làm những gì mọi người liên quan muốn nó làm.

Thật không may, điều này dẫn đến một mô tả dễ dàng về một nhiệm vụ dường như bất khả thi: phần mềm là đúng khi mọi người liên quan đều biết chương trình nên làm gì và có thể xác nhận rằng chương trình chỉ làm những gì nó nên làm. Theo một nghĩa nào đó, điều này là không thể. Có chương trình thực tế, nhưng sau đó còn có "Chương trình" (viết hoa). "Chương trình" là khái niệm sống trong đầu chúng ta. Đồng ý rằng một chương trình là đúng, theo một nghĩa nào đó, là đồng ý rằng chúng ta đều đang nghĩ cùng một suy nghĩ (tôi giả định điều này là không thể; tính khả thi về triết học của vấn đề này nằm ngoài phạm vi bài đăng này). Điều này dẫn đến một phiên bản kỹ lưỡng hơn của nhận định trước đó của tôi: một chương trình là đúng khi mọi người liên quan đồng ý rằng chương trình trong thế giới thực đang là một đại diện đầy đủ của "Chương trình" trong đầu họ và chương trình trong thế giới thực chỉ làm những gì nó nên làm. Vậy, làm sao chúng ta biết rằng chương trình hiện hữu chính là "Chương trình" chúng ta tưởng tượng?

Khái niệm mà tôi nghĩ đã giúp tôi nhất khi suy nghĩ về vấn đề này là "khoảng cách ngữ nghĩa" (semantic gap). Đối với tôi, khoảng cách ngữ nghĩa làm nổi bật những gì chúng ta đánh mất trong sự đánh đổi khi chuyển hóa các ý tưởng thành mã. Một số người có thể đọc mã, thấy rằng nó phản ánh "Chương trình" trong đầu họ, và nói "lgtm" (looks good to me - trông ổn đấy). Tôi nghĩ đó là mô hình lý tưởng khi sử dụng mã để giảm khoảng cách ngữ nghĩa giữa con người và các chương trình của chúng ta. Nhưng một số người sẽ đọc cùng một đoạn mã đó và nhận ra họ không có chút nào về cách nó kết nối với "Chương trình" trong đầu họ. Khi đã cạn kiệt các công cụ để giảm khoảng cách ngữ nghĩa và chịu áp lực phải giữ mọi thứ vận hành, chúng ta còn làm gì ngoài việc nghiêm túc gõ "lgtm"? Rõ ràng là đọc mã không thể là phương thức duy nhất để truyền đạt ý định của các ý tưởng đằng sau nó. Tuy nhiên, vào cùng lúc đó, tôi nghĩ mã thực thi có một lập luận thuyết phục để trở thành nguồn sự thật (source of truth). Nhưng nếu mã là một phương tiện giao tiếp kém hiệu quả ngay cả giữa các lập trình viên, chúng ta giúp mọi người hiểu các chương trình như thế nào? Tôi nghĩ đây chính là nơi phân tích chương trình (program analysis) phát huy tác dụng.

Cách tôi nghĩ về phân tích chương trình là nó là cách để tôi nhìn vào một chương trình mình đã viết, hỏi "mình đã làm gì", và nhận được kết quả có ý nghĩa. Có rất nhiều cách để làm điều này, và trong khi "chạy mã" là phổ biến nhất, nhánh phân tích tôi quan tâm được gọi là phân tích tĩnh (static analysis). Nó thú vị đối với tôi bởi vì, lý tưởng nhất, chúng ta có thể lấy một tập hợp các thành phần được chỉ định và đặt câu hỏi về toàn bộ hệ thống có khả năng làm gì mà không cần sử dụng tài nguyên liên quan đến việc chạy mã. Chương trình này có bao giờ cố gắng truy cập dữ liệu cụ thể không? Có cách nào để đến trang web này mà không cần đăng nhập không? Nói cách khác, có các quyết định cần được đưa ra trong mỗi chương trình và chúng tôi muốn xác nhận rằng những quyết định đó đang được thực hiện cẩn thận.

Nhưng các quyết định không phải lúc nào cũng được đưa ra một cách cô lập và không phải lúc nào cũng được đưa ra bởi những người có thể đọc mã để xác minh nó làm đúng việc. Khả năng kiểm tra các hệ thống — cung cấp câu trả lời nhất quán và chính xác cho các câu hỏi mà mọi người có về các chương trình đóng vai trò trong cuộc sống hàng ngày của chúng ta — là một điều cần thiết để từng có phần mềm đúng đắn. Ngay cả khi là tác giả của một chương trình, chúng ta cũng chỉ là một người mù chạm vào một phần của con voi. Chúng ta cần góc nhìn và sự hiểu biết của người khác để xác nhận chúng ta đã làm đúng việc.