> AIUI, in this case, the major issue is that it is very tempting to try to impose a constraint that all intermediate states the code passes through are semanti

> AIUI, in this case, the major issue is that it is very tempting to try to impose a constraint that all intermediate states the code passes through are semantically valid. However while superficially appealing this turns out to be a crippling constraint. This really isn't much of an issue in a language with holes as a first class concept, like Agda or Haskell.