Lambda the Ultimate

In a recent discussion about adding some dependent typing capabilities in BitC, it was proposed that we should instead statically reject programs that contain unsolved constraints, and require that the programmer take responsibility for inserting checks explicitly. The idea is that these checks can still be compiled out, but making them visible to the developer may have the effect of diagnosing bugs or inducing better arrangements of code. I'm not yet fully convinced, but I'm thinking about it. Here is the "catch" that I see:

When unsolved constraints lead to compile-time program rejection, the behavior of the solver becomes part of the language specification. It becomes necessary to specify a standard set of verification conditions that the compiler must generate (which seems straightforward), a standard rule base over which the solver must operate, and a standard behavior by which the solver must combine these rules. Individual implementations are certainly free to use better solvers, rule bases, or verification conditions but the language specification must define precisely what constitutes a "compliant" program, and compilers must retain the capability to identify programs that are not transportable (that is: programs that would not be accepted if the enhanced solver were not applied). Finally, if the language definition is to be deterministic, it would seem to follow that the reference solver must operate by exhaustive search, and must be assured to terminate.

So two questions:

• Am I overly conservative when I say that the solver must be exhaustive and terminating? Can a precise baseline language definition be had with weaker restrictions?

• Has there been any work on specifying solver behavior in this sort of way? By specifying, I mean in the sense of a reference language specification, but also in the sense that the language reference solver specification could be handled properly when the programming language is to be embedded in a prover for verification purposes?

  An ad hoc specification in the form of a reference implementation is certainly possible, but this seems like a pretty weak way to go about specifying a language. Particularly so if later program verification is desirable.

Anyway, what is the state of the art concerning solver specification?