5 ms·

why ocaml instead

• kevingadd 3y ago
  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.
  • JonChesterfield 3y ago
    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.