1. A method for validating at least a portion of a declarative program based on a background theory for a programming language having a type system that supports type test and refinement, including: for a given environment, translating a programming construct of the declarative program to at least one first order logic formula construct based on a semantic analysis; determining a validity of the at least one first order logic formula construct based on an analysis of the at least one first order logic formula construct; and determining whether a first type of the programming construct is a valid subtype of a second type of the programming construct based on the validity determination.