Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself. It would obviously help reduce errors but it wo

Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself. It would obviously help reduce errors but it wouldn't categorically eliminate them.