Incomplete Proofs and Program Synthesis

The theory of deductive program synthesis and verification relies on complete proofs of specifications. Such proofs are assumed to be found by an automated deduction program or constructed manually using a proof-checking system. This contradicts practice: even in mathematics most proofs are very far from being complete, and verification of programs usually checks only "principal" parts. Our goal here is to support this practice by some existing and new theory.