Why Formal

[ThePerfectComputer]

What makes this codebase a formal model? I ask because I'm currently writing a model for a CPU I'm designing in Haskell, and I want to know what a model has to have to be called "formal".

[samuelgruetter]

It's formal in the sense that it enables its users to apply formal methods, ie to reason with mathematical proofs about the behavior of their hardware and/or software. You can read more about how we did that in this preprint paper.

[ThePerfectComputer]

Oh wow! That paper is really cool. Incidentally, I have been using Clash for some other projects.

[ThePerfectComputer]

Lines like these seem a bit verbose and redundant...
https://github.com/mit-plv/riscv-semantics/blob/master/src/Spec/Decode.hs#L17-L21

I could conceive of perhaps:

data LoadType = LoadType  { rd :: Register, rs1 :: Register, oimm12 :: MachineInt }

data InstructionI =
  Lb LoadType |
  Lh LoadType |
  Lw LoadType |
  Lbu LoadType |
  Lb LoadType |
  Lhu LoadType

Why such a verbose approach?

[ThePerfectComputer]

Also - perhaps this isn't the appropriate place for this conversation. I'm genuinely intrigued by this codebase at a basic level - and I suppose I have a number of questions...