Mục lục
Ghi Chép Nhỏ Trong Đầu Khi Viết Code
Trong quá trình phát triển sự nghiệp lập trình, tôi vô tình phát hiện một mẹo giúp viết code nhanh và chính xác hơn. Nghe thì có vẻ đơn giản, nhưng thực hành thành thạo lại đòi hỏi nhiều nỗ lực: đó là hình thành các chứng minh logic ngắn gọn trong đầu khi code.
Khi đối mặt với vấn đề phức tạp, hãy tự vẽ ra lập luận chứng minh code của bạn sẽ hoạt động như mong đợi. Khi thuần thục kỹ thuật này, bạn sẽ ngạc nhiên khi thấy code chạy đúng ngay từ lần đầu hoặc thứ hai – cảm giác gần như ma thuật!
5 Kỹ Thuật Tư Duy Logic Cho Lập Trình Viên
1. Nguyên Tắc Đơn Điệu Trong Code
Khái niệm “code đơn điệu” mô tả các quy trình chỉ tiến triển theo một hướng. Ví dụ điển hình là cơ chế checkpointing:
- Script thực thi tuần tự nhiều tác vụ
- Lưu trạng thái hoàn thành trên disk
- Khi crash, script tiếp tục từ bước chưa hoàn thành
Trong hệ thống database, LSM-tree là ví dụ tuyệt vời về tính đơn điệu khi chỉ thêm mới dữ liệu thay vì sửa đổi tại chỗ như B-tree. Cấu trúc immutable (bất biến) cũng là “anh em” với tính đơn điệu – giúp loại bỏ ngay lập tức các kịch bản thay đổi ngoài ý muốn.
2. Điều Kiện Tiên Quyết và Hậu Điều Kiện
Đây là cách xác định ràng buộc cho hành vi của hàm:
- Điều kiện tiên quyết: Những yêu cầu phải thỏa mãn trước khi hàm chạy
- Hậu điều kiện: Cam kết đúng sau khi hàm kết thúc
Xác định hậu điều kiện chính xác giúp sinh ra các unit test chất lượng. Thêm assertion kiểm tra các điều kiện này giúp chương trình crash sớm khi có lỗi – vẫn tốt hơn hành vi không thể đoán trước.
3. Bất Biến (Invariants) – Nền Tảng Của Hệ Thống Ổn Định
Invariant là tính chất luôn đúng dù code chạy thế nào. Ví dụ kinh điển là phương trình kế toán:
- Tổng nợ phải bằng tổng có trong sổ sách
- Mỗi giao dịch bảo toàn cân đối này
Cách đơn giản để đảm bảo invariant là chia code thành các bước nguyên tử, chứng minh mỗi bước giữ nguyên tính bất biến. Kỹ thuật lifecycle methods (như constructor/destructor trong C++ hay useEffect trong React) cũng giúp duy trì invariant.
4. Kỹ Thuật Cách Ly Thay Đổi
Phần lớn nghệ thuật phát triển phần mềm nằm ở việc mở rộng hệ thống hiện có mà không phá vỡ chức năng cũ. Mỗi thay đổi có “bán kính ảnh hưởng” nhất định – điểm mấu chốt là xác định các “bức tường lửa” ngăn thay đổi lan rộng.
Ví dụ từ hệ thống Nerve:
- Cơ chế xử lý trường ảo (virtual fields)
- Hai cách tiếp cận: sửa đổi toàn bộ pipeline hoặc dùng kỹ thuật over-pulling
- Lựa chọn sau giới hạn thay đổi ở hai lớp đầu cuối, giữ nguyên phần core
Nguyên tắc Open-Closed khuyến khích mở rộng bằng code mới thay vì sửa code cũ đang hoạt động.
5. Quy Nạp Toán Học Cho Code Đệ Quy
Cấu trúc đệ quy (như tree) và hàm đệ quy rất phổ biến. Để chứng minh tính đúng đắn, quy nạp toán học là vũ khí lợi hại gồm:
- Chứng minh trường hợp cơ sở (base case)
- Chứng minh nếu đúng với n thì đúng với n+1 (bước quy nạp)
Áp dụng vào hàm simplifyTree xử lý AST:
- Base case: node lá không thể contract (đã thoả mãn)
- Bước quy nạp: giả sử đúng với mọi subtree thì sẽ đúng với cả tree
Cải Thiện Chất Lượng Code Qua Khả Năng Chứng Minh
Tôi gọi đặc tính này là “proof-affinity” – mức độ dễ dàng lập luận về tính đúng đắn của code. Proof-affinity cao đồng nghĩa với:
- Cấu trúc code rõ ràng
- Logic dễ theo dõi
- Ít bug tiềm ẩn
Đây không phải tiêu chí duy nhất nhưng cực kỳ quan trọng vì muốn cải tiến hệ thống, trước hết phải hiểu nó hoạt động thế nào.
Luyện Tập Nâng Cao Kỹ Năng
Để thành thạo tư duy chứng minh:
- Viết nhiều chứng minh toán học (đừng chỉ đọc)
- Tham gia khoá học thuật toán có tính chứng minh
- Giải Leetcode tập trung vào độ chính xác thay vì tốc độ
Kỹ năng này như touch-typing – chỉ phát huy khi trở thành phản xạ. Không có đường tắt, chỉ có luyện tập kiên trì!
