Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

You’re saying there is a bug in the spec they are verifying against?

Yes. But they aren't verifying their spec against anything (yet). Their primary focus is on proofing abstract properties of the ISA..

And that is also very important of course, but I think the first step should be proving that the spec actually matches the implementation.

But but but... all the hard bits of specs and of processors are in exception handling. If you skip that bit, you’re doing the easy 10%

Why would you write spec in a language that many programmer find obscure and hard (for humans) to parse???

I asked exactly that question in the workgroup. Answer: Target audience is formal people, for them Haskell is easy. (paraphrased)

Target audience should include asm programmers, people writing tests, people writing compilers and OS, hardware designers, ...