Interestingly, allowing the internal block structure
can increase the difficulty of doing logic on
the code to the point where building proof tools become
NP-complete (or at least insanely hard).
This is relevant if you're tying to use static analysis
tools, not just if you're trying to prove theoroms (;-))
--dave (who proveth not, but analyzeth a lot) c-b