1. A method for testing at least one type of declarative program, the method executable by a processor, the method including: receiving declarative program according to a declarative programming model and a declarative data scripting language implementing a type system supporting constraint-based refinement type statements, that test an evaluation of an expression for membership of an indicated type, the declarative program including a plurality of programming constructs; interpreting and verifying validity of the plurality of programming constructs according to rules defined based on the type system by, for each programming construct of the plurality of programming constructs and based on the rules, performing a synthesis step on the programming construct that receives at least an expression as input and outputs a type for the expression or indicates an error; and performing a type checking step that receives the expression and the type as input and outputs true if the type is valid for the expression or false if the type is invalid for the expression, wherein the synthesis step is performed according to a first judgment form based on a function having inputs of a context and an expression and that returns either a type or fails, and wherein the type checking step is performed according to a second judgment form based on a function having inputs of a context, an expression and a type and that returns either true or false.