[JonChesterfield]

I'm slowly coming around to SML and HOL as the best available tools for stuff like the op. In particular cakeml and candle look suspiciously like a solid foundation for modelling instruction sets.