How do empirical tests compare to proofs?

The mainstream technical view distinguishes what the methods establish. Tests execute selected cases and can reveal bugs, environmental problems, or incorrect assumptions; they are valuable for behavior that is difficult to model. Proofs can establish universal properties over a formal model, but only relative to its assumptions and specification. In software engineering, the strongest practical position in these sources is complementary use: tests provide concrete feedback and proofs provide broader deductive assurance.

• Tests examine selected executions or observations, so they can discover failures but do not generally establish correctness across all possible inputs.
• Proofs can guarantee a property for all executions covered by the formal model and assumptions.
• A proof does not by itself secure properties excluded by its assumptions, such as an untrusted runtime or compiler.
• Proof failures can be converted into concrete tests through prover-generated counterexamples, making the methods operationally complementary.

A dissenting methodological view resists treating formal proof as uniquely certain in practice. Many proofs are high-level arguments whose details and reliability vary, and formal verification of real programs can be costly because specifications, programs, and requirements change. From this perspective, proof is exceptionally strong evidence within a framework, but empirical testing and other forms of evidence may be more informative or manageable for particular questions.

• In ordinary mathematical practice, many accepted proofs are high-level explanations rather than completely checked low-level derivations, and some later prove mistaken.
• Treating proofs as strong evidence allows the required level of detail to vary with context and leaves room for other evidence-generating methods.
• Formal verification can be difficult to justify for real programs because specifications are complex and programs and requirements change.
• The operational execution-focused approach may be technically weaker than reasoning from program text and specifications, according to a contrasting programming-methodology argument.
• Practical critics argue that formal verification may be impractical or wasteful outside suitable niches, despite renewed interest in it.