Lambda the Ultimate

Microsoft recently demoed a very interesting system for kids called Kodu. Kodu lets kids 'program' their own games for Xbox 360.

The language lets kids write programs like this:
when [game-pad] [left-click] do [fire] [at-monster]

Except game-pad, left-click, etc. are cartoonish icons kids pick out from context relevant lists.

This summary is based on watching two videos, at most a few minutes in length :) The video in the link is probably most relevant. There doesn't seem to be any more technical detail available on the web.

Wadler, for instance, makes the claim, in "The marriage of effects and monads" (pg. 1), that effects typing systems are usually found in strict languages, whereas monads are usually found in lazy languages. Why is this? Is there a technical reason, or just a difference in cultures between the two camps?

(I have seen others make an even stronger claim, that monads are especially suited for lazy languages, in some sense.)

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?