Cách trở thành lập trình viên giỏi hơn bằng cách thực hiện những chứng minh nhỏ trong đầu

 (the-nerve-blog.ghost.io)
1 điểm bởi GN⁺ 2025-07-16 | 1 bình luận | Chia sẻ qua WhatsApp
  • Để trở thành một lập trình viên giỏi hơn, điều quan trọng là hình thành thói quen tự vẽ ra những chứng minh nhỏ trong đầu khi viết code
  • Tính đơn điệu, tính bất biến, tiền điều kiện - hậu điều kiện, và các bất biến là những khái niệm cốt lõi khi thực hiện các chứng minh mini như vậy
  • Thiết kế có tính đến phạm vi ảnh hưởng của thay đổi mã lên toàn bộ hệ thống (cô lập, tường lửa) giúp giảm đáng kể độ phức tạp và rủi ro
  • Có thể dùng quy nạp để chứng minh tính đúng đắn của hàm đệ quy hoặc cấu trúc theo từng bước
  • Kiểu tư duy này được rèn luyện qua thực hành và hình thành thành thói quen; việc luyện chứng minh toán học và giải bài toán thuật toán trong thực tế rất hữu ích

Giới thiệu và ý tưởng cốt lõi

  • Tác giả cho biết khi tích lũy kinh nghiệm, họ đã tự nhiên hình thành “thói quen vẽ ra những chứng minh nhỏ” để nâng cao độ chính xác và tốc độ khi viết code
  • Quá trình kiểm chứng và suy luận hành vi dự kiến trong đầu khi lập trình cần được rèn luyện, và khi thành thạo thì chất lượng hoàn thiện của code sẽ cải thiện rõ rệt
  • Cách thực hiện cụ thể không quá quan trọng; có thể luyện theo nhiều cách khác nhau sao cho phù hợp với bản thân

Tính đơn điệu (Monotonicity)

  • Tính đơn điệu (monotonicity) là tính chất mà hàm hoặc code chỉ tiến triển theo một hướng
  • Ví dụ là checkpointing: tiến trình công việc chỉ đi về phía trước và không quay lại để chạy lại phần việc đã xong
  • Trong ví dụ so sánh LSM tree với B-tree, LSM tree có đặc tính phần lớn dung lượng chỉ tích lũy thêm và chỉ giảm trong quá trình compaction
  • Khi tính đơn điệu được đảm bảo, ta có thể tự nhiên loại trừ hoặc dự đoán một số trạng thái hay kết quả phức tạp
  • Tính bất biến (immutability) cũng là một khái niệm tương tự, vì một khi giá trị đã được thiết lập thì sẽ không bao giờ thay đổi, từ đó loại bỏ khả năng biến đổi trạng thái

Tiền điều kiện và hậu điều kiện (Pre- and post-conditions)

  • Tiền điều kiện (pre-condition) và hậu điều kiện (post-condition) là những khẳng định bắt buộc phải đúng trước và sau khi hàm được thực thi
  • Việc theo dõi rõ ràng các điều kiện này khi viết hàm sẽ hỗ trợ tư duy logic và kiểm thử
  • Khi xác định rõ hậu điều kiện, việc suy ra các test case cho unit test cũng trở nên dễ dàng hơn
  • Việc thêm assertion vào code để kiểm tra các điều kiện này và dừng sớm khi gặp tình huống bất ngờ sẽ làm tăng tính dự đoán được và độ an toàn
  • Cũng có những trường hợp rất khó gán tiền điều kiện hoặc hậu điều kiện rõ ràng cho một hàm, và bản thân việc phát hiện điều đó cũng mang lại nhiều gợi ý quan trọng

Bất biến (Invariants)

  • Bất biến là thuộc tính phải luôn đúng trong mọi tình huống: trước, trong và sau khi code chạy
  • Một ví dụ điển hình là phương trình kế toán trong hệ thống kế toán kép (tổng bên Có = tổng bên Nợ)
  • Nếu tách toàn bộ code thành các bước nhỏ và chứng minh rằng mỗi bước đều bảo toàn bất biến, ta có thể đảm bảo tính toàn vẹn của toàn hệ thống
  • Có những cách dùng listener hoặc lifecycle method để duy trì bất biến, chẳng hạn constructor/destructor trong C++ hay useEffect của React
  • Khi số lượng thay đổi ít hoặc đường đi xử lý đơn giản, việc kiểm chứng bất biến sẽ dễ hơn rất nhiều

Cô lập (Isolation)

  • Một trong những cốt lõi của phần mềm tốt là có thể thêm hoặc sửa tính năng mới mà không làm hệ thống hiện có trở nên kém ổn định
  • Cần xác định “bán kính ảnh hưởng” (blast radius) của thay đổi code và tạo ra các “tường lửa” cấu trúc để giảm thiểu phạm vi lan truyền của tác động
  • Bài viết giới thiệu ví dụ từ dịch vụ Nerve: xác định rõ ranh giới giữa query planner và query executor, rồi thiết kế sao cho phần thay đổi không vượt qua ranh giới đó
  • Nếu ngăn được sự lan truyền thay đổi không cần thiết, việc kiểm chứng và bảo trì sẽ dễ hơn, đồng thời độ ổn định cũng cao hơn
  • Điều này cũng tương đồng với triết lý của OCP (Open-Closed Principle): mở rộng tính năng mà không thay đổi hành vi hiện có

Quy nạp (Induction)

  • Nhiều chương trình có chứa hàm đệ quy hoặc cấu trúc đệ quy, và quy nạp là công cụ rất mạnh để xây dựng lập luận cho chúng
  • Để chứng minh từng bước hoạt động và tính đúng đắn của hàm đệ quy, cần xác minh riêng trường hợp cơ sở (base case) và bước quy nạp (inductive step)
  • Bài viết lấy ví dụ về quá trình đơn giản hóa node trong cấu trúc AST (cây cú pháp), và dùng lập luận quy nạp theo từng bước để chứng minh việc bảo toàn bất biến cũng như tính đúng đắn của hành vi
  • Khi tư duy quy nạp đã trở nên tự nhiên, việc viết và kiểm chứng code đệ quy sẽ trực quan và dễ dàng hơn nhiều
  • Tác giả cũng gợi ý so sánh cách này với nỗ lực kiểm chứng toàn cục (holistic) không theo quy nạp để suy ngẫm xem cách nào tự nhiên hơn

Proof-affinity (độ thân thiện với chứng minh) như một chỉ số chất lượng

  • Tác giả lập luận rằng code tốt là loại code mà ta có thể vẽ ra những chứng minh nhỏ trong đầu
  • Nếu code có các cấu trúc như tính đơn điệu, tính bất biến, điều kiện rõ ràng, phân tách bất biến, ranh giới kiểu tường lửa, hay vận dụng quy nạp, thì nó thực sự dễ chứng minh hơn, và vì thế bản thân code cũng có chất lượng cao hơn
  • Nếu code đang ở trạng thái khó hiểu và khó kiểm chứng, đó là dấu hiệu cho thấy cần refactor hoặc xem xét lại cấu trúc
  • Trong ngữ cảnh này, tác giả đề xuất dùng thuật ngữ proof-affinity thay cho “khả năng chứng minh”
  • Proof-affinity không phải là yếu tố duy nhất quyết định chất lượng phần mềm, nhưng là chất xúc tác rất quan trọng cho việc hiểu, mở rộng, kiểm thử và bảo trì code

Cách nâng cao năng lực

  • Kiểu tư duy logic này chỉ trở nên tự nhiên một cách vô thức khi được rèn luyện đủ nhiều
  • Việc thường xuyên viết chứng minh toán học và trau dồi năng lực suy luận logic là điều thiết yếu
  • Giải các bài toán thuật toán (như khóa học EdX của Stanford, Leetcode, v.v.) cũng là môi trường luyện tập rất tốt; nên tập trung vào những bài không chỉ đòi hỏi mẹo mà còn cần triển khai cẩn thận và tư duy mang tính chứng minh
  • Thay vì sửa kết quả đi sửa lại nhiều lần mới đúng, điều quan trọng là luyện cách tiếp cận gần đáp án đúng ngay từ lần đầu
  • Thông qua việc hình thành những thói quen như vậy, năng lực thiết kế hệ thống logic và chất lượng code có thể được cải thiện rất lớn

Bài viết liên quan

1 bình luận

 
GN⁺ 2025-07-16
Ý kiến trên Hacker News

  • Có một ví dụ rất hợp với chủ đề này, vừa đơn giản vừa đáng ngạc nhiên: tìm kiếm nhị phân. Có cả biến thể trái/phải, nhưng nếu không suy nghĩ về bất biến vòng lặp thì rất khó triển khai cho đúng. Bài viết này giải thích cách tiếp cận bằng bất biến cùng ví dụ mã Python tương ứng. Jon Bentley, tác giả của Programming Pearls, từng yêu cầu các lập trình viên IBM cài đặt tìm kiếm nhị phân thông thường, và 90% có lỗi. Phần lớn là lỗi rơi vào vòng lặp vô hạn. Thời đó còn phải tự tránh tràn số nguyên nên cũng phần nào dễ hiểu, nhưng tỷ lệ đó vẫn rất đáng kinh ngạc

    • Sau khi thấy điều này, tôi bắt đầu dùng tìm kiếm nhị phân làm câu hỏi phỏng vấn. Khoảng 2/3 ứng viên có tiếng mà tôi gặp không thể viết được một bản cài đặt chạy đúng trong vòng 20 phút. Đặc biệt hay bị mắc vào vòng lặp vô hạn ở các trường hợp dễ. Những người làm được thì thường viết rất nhanh. Một phần nguyên nhân là nhiều người học từ giao diện sai. Ngay cả Wikipedia cũng giải thích là "khởi tạo L bằng 0, R bằng n-1", tức là dùng khoảng có bao gồm R. Trong thực tế, với đa số thuật toán xử lý chuỗi, dạng không bao gồm cận trên, tức R = n, lại tốt hơn. Tôi muốn tự kiểm chứng giả thuyết này: cho nhiều người viết với các prototype hàm và giá trị khởi tạo khác nhau, rồi so sánh tỷ lệ lỗi giữa cận trên inclusive, exclusive và cách dùng độ dài

    • Thực ra tìm kiếm nhị phân gần như là ví dụ tiêu biểu khó quản lý chỉ số nhất. Cùng với thuật toán phân hoạch Hoare, đây là một trong những thuật toán cơ bản khó viết chính xác mà không mắc lỗi nhất

    • Tôi thử nhờ Claude Sonnet viết mã Python tìm kiếm nhị phân không lỗi

    def binary_search(arr, target):
    left = 0
    right = len(arr) - 1
    while left <= right:
        mid = left + (right - left) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

    Tôi cũng kiểm tra nhiều test case khác nhau với mảng ví dụ

    • Biết rằng lỗi trong tìm kiếm nhị phân nổi tiếng đến mức trở thành một ví dụ điển hình sai lệch, tôi từng thử đưa bản cài đặt không lỗi đầu tiên của mình vào sách. Tôi đã viết cực kỳ cẩn thận mà cuối cùng vẫn có lỗi, nên thấy khá buồn cười. May là nhờ hệ thống phản hồi sớm của Manning mà tôi sửa được trước khi in

    • Tôi luôn cài đặt tìm kiếm nhị phân trái/phải theo kiểu ghi nhớ "giá trị tốt nhất cho đến thời điểm hiện tại". Tức là cách giống lower_bound, upper_bound trong C++. Với cấu trúc while (l < r), ta tìm điểm giữa rồi kiểm tra vị trí hiện tại để điều chỉnh phạm vi cho phù hợp. Ví dụ với upper_bound thì nâng cận trái lên, còn lower_bound thì hạ cận phải xuống. Lâu rồi mới làm lại leetcode nên đầu óc hơi mụ mị, định dạng có thể hơi lộn xộn

  • Hình như từ lâu tôi đã biết một khái niệm tương tự trong lớp cao học. Từ khoảng cuối thời đại học, tôi làm bài thi toán hoàn toàn bằng bút mực. Tôi cũng không rõ vì sao, nhưng điểm số luôn cao hơn, vì tôi phải giải tuần tự một lần và hình dung trọn vẹn quá trình chứng minh trong đầu rồi mới viết ra. Nhờ vậy tôi mắc ít lỗi hơn nhiều. Khi code tôi cũng làm tương tự: thiết kế cho thật hoàn chỉnh trong đầu rồi mới bắt đầu

  • Muốn trở thành lập trình viên giỏi hơn, bạn nên rèn thói quen viết những chứng minh nhỏ cho mã của mình Test và định nghĩa kiểu chính là những ví dụ điển hình của hành vi đó Đặc biệt, tôi thường tiếp cận theo thứ tự: viết test trước, sau đó là kiểu, cuối cùng mới đến code Nên tạo test cho từng acceptance criteria, với đầu vào/đầu ra được mô tả rõ ràng Nếu là API thì có thể viết đặc tả trước bằng OpenAPI hoặc GraphQL, bao gồm toàn bộ thuộc tính và kiểu. Ở runtime có thể xác thực dữ liệu dựa trên đặc tả này, và bản đặc tả đó tự nó đã là một chứng minh rằng ứng dụng vận hành theo đúng đặc tả Tóm lại, điều quan trọng là phải có được bằng chứng rằng hệ thống thực sự hoạt động như mong muốn thông qua OpenAPI/GraphQL, test và kiểu Nếu bản đặc tả được thiết kế tốt ngay từ đầu, thì việc thay đổi phần cài đặt code vẫn linh hoạt mà vẫn có thể chứng minh tính đúng đắn bằng đặc tả Đặc tả quan trọng hơn bản thân code

    • Năm thuộc tính được nhắc đến trong bài đều có thể biểu diễn trong một hệ thống kiểu tốt. Theo cách này, phần lớn đặc tả trở thành code, và compiler đảm bảo tính đúng đắn. Tương lai của lập trình nên đi theo hướng cách tiếp cận này trở thành điều hiển nhiên Hệ thống kiểu của OpenAPI và GraphQL quá nghèo nàn, nên để tới được tương lai đó có lẽ còn phải phát triển thêm 50 năm nữa

  • Tôi đã học nền tảng khoa học máy tính lý thuyết ở đại học và rất đồng cảm với tinh thần của bài này. Chỉ là thực hành thì không dễ Ngoài tiền điều kiện/hậu điều kiện, các kỹ thuật chứng minh trong CS như bất biến vòng lặp (loop invariant), quy nạp cấu trúc (structural induction) cũng cực kỳ mạnh Kèm theo các liên kết loop invariant, structural induction, tôi cũng muốn giới thiệu ghi chú môn CSC236H của UofT (ghi chú bài giảng)

    • Ghi chú môn CSC236 này rất xuất sắc, và giáo sư David Liu cũng là một người rất tuyệt giới thiệu giáo sư

    • Có nhắc tới UofT kìa! Vui thật

  • Ý tưởng "tự tạo những chứng minh nhỏ trong đầu về code" là một nguyên tắc quan trọng đến mức gần như phải xem là hiển nhiên. Bạn luôn nên ý thức một mệnh đề đơn giản về việc từng phần trong code đang làm gì

    • Tinh thần này thì dễ áp dụng trong các dự án greenfield, nơi gần đây bạn tự viết toàn bộ mã, nhưng với codebase thực tế nơi nhiều người cùng chạm vào đủ loại hàm và trạng thái toàn cục thì thấy khó hơn nhiều

      • Một lập trình viên thực sự giỏi là người có thể dần đưa hệ thống tiến về hướng đó. Code ngoài đời thì lộn xộn, nhưng điều quan trọng là phải từ từ thu hẹp các lỗ hổng trong bất biến, đồng thời tạo ra cấu trúc code giúp những người đến sau cũng nhận thức được các bất biến và thuận lợi trong việc duy trì chúng. Tài liệu có ích, nhưng theo kinh nghiệm của tôi, chính cấu trúc code còn quan trọng hơn

      • Thực ra đây chính là lý do mang tính quyết định khiến trạng thái toàn cục nguy hiểm. Muốn chứng minh tính đúng đắn của code thì phải biết cả chương trình. Nếu biến giá trị toàn cục thành bất biến, hoặc truyền nó qua tham số hàm, hoặc quản lý bằng một lớp bọc trạng thái, thì chỉ cần nắm rõ các caller của hàm đó là đủ. Nếu thêm các ràng buộc như assertion bên trong hàm thì độ khó của việc chứng minh giảm đi rõ rệt. Rất nhiều lập trình viên đã và đang đưa ra các quyết định như vậy, chỉ là họ làm theo bản năng chứ không ý thức đó là vì mục tiêu chứng minh

      • Code mà nhiều lập trình viên cùng quản lý trạng thái toàn cục có thể ví như một bệnh nhân "ung thư đã di căn". Việc chữa trị khó hơn nhiều, và đôi khi có cứu được hay không còn phụ thuộc vào may mắn và điều kiện bên ngoài

      • Đúng như bài viết nói, loại code này có xác suất sinh lỗi cao hơn rất nhiều, và rủi ro phát sinh lỗi mới trong quá trình bảo trì cũng lớn. Điều đó cho thấy viết ngay từ đầu theo cấu trúc có thể chứng minh được là con đường đúng đắn hơn nhiều

      • Đọc bài này làm tôi nghĩ đến việc mình liên tục tự xem lại cách code, cố gắng tái định hình theo hướng tốt hơn. Tôi cũng tự hỏi những người như John Carmack, theo thời gian, có cảm thấy code cũ của mình còn nhiều thiếu sót và dần hình thành cảm giác làm mọi thứ "tốt hơn" hay không

  • Ý tưởng code phải có thể chứng minh được đã xuất hiện từ khi Dekker giải bài toán mutual exclusion năm 1959. Một giai thoại thú vị về chuyện này được kể trong bài EWD1303 của Dijkstra (liên kết gốc). Có thể xem các nghiên cứu tiếp theo của Dijkstra cũng là sự tiếp nối của chính trực giác đó

  • Viết ra một chứng minh đúng thực sự rất khó. Kiểm chứng chương trình cũng không hề dễ. Theo tôi, nếu cố làm chứng minh thủ công thì không hiệu quả. Nếu viết code theo đúng lối idiomatic của ngôn ngữ và codebase tương ứng thì thường không cần quá bận tâm đến bất biến hay tiền/hậu điều kiện. Tinh thần "đơn giản, rõ ràng, tổng quát" mà R. Pike và B. W. Kernighan nhấn mạnh trong "The Practice of Programming" có hiệu quả rất lớn trong thực tế. Hơi liên quan nhưng là câu chuyện khác: nếu từng làm competitive programming, bạn sẽ phải nắm thật chắc các kỹ thuật đảm bảo tính đúng đắn của code thì mới lên được trình cao hơn

    • Tôi không đồng ý với điều này. Theo tôi, điều tác giả bài viết muốn nói không phải là chứng minh hình thức hoàn chỉnh, mà là bạn nhất định phải suy nghĩ về những thuộc tính logic nào đang được đảm bảo bởi code của mình, ví dụ như bất biến. Chính quá trình đó là con đường tốt nhất để hiểu code và vượt qua cảm giác sợ hãi trước nội dung của nó

    • Ở đây có vẻ đang đảo ngược nguyên nhân và kết quả. Nếu tiếp cận vấn đề một cách cẩn thận và suy nghĩ kỹ, thì hệ quả tự nhiên là code cũng sẽ rõ ràng và gọn gàng hơn. Logic rõ ràng thì thiết kế code cũng rõ ràng theo. Nhưng tin rằng chỉ cần viết code đẹp là tự nhiên tính đúng đắn sẽ đi kèm thì không hợp lý. Dĩ nhiên code càng sạch thì càng giảm bug trong review và những khâu tương tự. Cần nhớ rằng hình thức phải theo sau chức năng

    • Khái niệm cơ bản nhất của chứng minh là "cơ sở để biết tại sao cái này đúng". Nó không chỉ để tránh các lỗi vặt, mà là quá trình xác nhận rằng định hướng nền tảng có đúng hay không

    • Để code đúng thì không có con đường thay thế nào khác ngoài việc viết nó cho đúng. Dù khó đến đâu cũng phải viết cho đúng

    • Nếu lật ngược hẳn đoạn đầu, có thể nói rằng với các trừu tượng phù hợp — tức code idiomatic đúng với ngôn ngữ/codebase — thì việc kiểm chứng chương trình trở nên dễ hơn. Vì trong những trừu tượng phù hợp đó, bạn không cần nghĩ về bất biến vòng lặp các kiểu nữa, nên từ tính đúng đắn của code, chứng minh sẽ theo ra ngay

  • Tính khả biến và bất biến (mutable/immutable) cũng là các thuộc tính quan trọng. Càng giữ trạng thái bất biến tối đa thì không chỉ đa luồng mà cả việc suy luận về trạng thái chương trình cũng bớt phức tạp hơn

    • Bài gốc thực ra đã có nói đến điều này rồi

  • Hồi còn là sinh viên đại học ở Carnegie Mellon vào những năm 80, tôi đã được dạy rất rõ về các nguyên tắc này. Sau đó nó giúp ích rất nhiều cho cuộc đời tôi. Đặc biệt, tôi còn nhớ khoảnh khắc học được sự tương đương giữa đệ quy và quy nạp, từ đó có thể tiếp cận thuật toán đệ quy một cách gọn gàng thay vì kiểu "thử bừa cho tới khi ra đáp án"

    • Gần đây tôi mới học lớp đó, và khi học lập trình hàm thì còn ngộ ra mạnh hơn nữa