Tìm các sai sót bằng cách nào?
Một câu hỏi khó! Điều mà nhà lập trình bận tâm là tạo ra một công việc không có lỗi, nhất là trong một thời gian hợp lý. Vì vậy người ấy soạn chương trình, nhận thấy rằng mình không thu được kết quả mong đợi (thậm chí không kết quả gì), tìm sai sót và bắt đầu lại. Người ấy có thể tự giúp mình bằng một debugger (từ cùng họ với déboguer/debug - loại bỏ sai sót), là phần mềm thực hiện chương trình từng bước, vận hành từng bước, để giúp tìm ra lỗi lầm. Các xét nghiệm này là cần nhưng rất đắt: người ta thường cho rằng phải có bốn người lập trình xét nghiệm, sửa chữa và duy trì cái mà một người đã lên chương trình. Một người lập trình phải dành 80% thời gian để loại bỏ sai sót.
Lao động này của người gây dựng không làm hài lòng nhà lý thuyết. Một chương trình có thể đối mặt với một tình huống bất ngờ và “chốt” ở đấy. Muốn tin chắc một chương trình là đúng phải dựa vào toán học. Thận trọng đầu tiên là đảm bảo rằng chương trình không thể chơi vơi, vô ích. Trên thực tế, tất cả các ngôn ngữ vẫn có khả năng lặp lại một công việc trong khi chờ đợi một kết quả chính xác. Nếu không có kết quả này thì sao? Chương trình mò mẫm ứng biến mà vẫn không sao thoát khỏi vòng luẩn quấn. Tiếc rằng không thể soạn một chương trình kiểm tra có khả năng đoán trước những biểu hiện này từ văn bản của chương trình được xét nghiệm. Phải chứng tỏ được sự kết thúc theo từng trường hợp, chẳng hạn phân biệt trong chương trình một giá trị không ngừng giảm đi cho tới khi bằng 0. Để chứng minh câu trả lời hoặc đáp án là đúng, phải để cho các nhà ngữ nghĩa học đưa ra một ý nghĩa toán học cho từng chỉ dẫn của chương trình. Vì vậy có những ngôn ngữ hỗ trợ cho bằng chứng, tự động hoặc bán tự động (mà đôi khi phải hướng dẫn không). Các kỹ thuật này có liên quan với những hoạt động cần đến sự an toàn, như trong ngành hàng không hoặc công nghiệp vũ trụ (trường hợp vụ nổ Arianea 5).
