I remember in 1982 or 1983 we had a very very slow implementation of Ada on our university VAX that was written at NYU as an executable specification in a language called SETL.
I don't think it was a formal decision that got made at any point, so there wasn't any particular reason. When someone else started writing the actual spec he picked Ocaml. It ended up probably being the wrong choice in the short term (we had to reimplement 32-bit floats in software, and for a while we couldn't run the ocaml files on windows very easily) but in the long term it seems like it worked out OK.
I kind of wish we had used a theorem prover language of some sort though since we had the opportunity to do so. I didn't really have the chance to change things there since other people had higher seniority than me.
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.