safeD formal semantics

[BCS]

Looking at this: http://blog.regehr.org/archives/249 

Prediction 4: Formal Semantics Will Be Constructed Earlier

How much of safeD is formalizable? Is there anything in it that is hoplessly 
impractical to create formal semantics for?

--
... <IXOYE><