Lambda the Ultimate

Dear all, I fear this may be a really strange question, but LtU seems the best place to ask it anyway. I am working on a programming language, Casanova, built for interactive applications and games in particular. The language is built in order to enable applications to implicitly update their state with continuously run "rules" which can also be suspended easily. For example, a lightswitch would be implemented quite easily as:

world LightSwitch = {
  Sprite  : Sprite
  Pressed : bool
  rule Pressed = 
    when(IsKeyDown(Keys.Space))
    yield true
    yield false
    when(IsKeyUp(Keys.Space))
  rule S.Color = 
    yield Color.White
    when Pressed
    yield Color.Black
    when Pressed
}

I would like to try and formalize why this approach is better than existing patterns commonly found in the literature for encoding state machines. I do not wish to do a survey of existing techniques and count lines of code or number of statements. This is clearly a viable approach, but for once I would like to go formal instead of empirical.

My goal is to show a way to encode the program above in a simple imperative language. I would then like to prove that this encoding is minimal with respect to the number of statements used. Finally, I would like to show that the encoding produces code which contains far more statements than the Casanova implementation.

The issues I have are: I have no clue how to go with a proof of minimality for some encoding, and I wonder if the overall approach sounds convincing to you guys.