I completely agree. And I specifically draw your attention to the fact that this is not a formal verification, which it would be reasonable to do: Coq, Isabellll, Agda, F* etc. However, Formal Specification. Those. representation of the specification in a formalized form. Haskell example: https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec
In this case, the term "formal" refers to the formalization of the representation of the specification. And it seems to be already established.
You can easily import and use specific functions for the decoder, or executor for specific ISA. Or even use the whole state machine. And this is represented by tests. Those. any single RISC-V architecture instruction, or an entire program. Because it can be used as a cpu emulator. Those. OS doesn't matter in this case. However, I draw your attention to the fact that this is only a processor, and not an emulation of the PC and its peripherals.
It's possible to emulate. But not only. The main goal is to formalize the representations of the RISC-V instruction set (ISA), decoder, executor, and state machine. So it's more formal point of view for RISC-V ISA.
The main competitor of Haskell, and also not the most popular language. However, the only way to popularize a language is to write in it. This project is trying to reveal the possibility of F#, and show the worthy side of F#,
Due to the properties of F# as a functional language, using a pure representation of functions and a strong type system - in this case, this is a formalization of RISC-V ISA (instruction set). Since we don't have side effects for pure functions.
As it has a State machine, one fun opportunity is to execute elf-bin files for it for RISC-V architecture.
I'm not sure what do you mean "compile programs", because it's not the compiler.
Since F# is a functional language, it allows, using a purely functional approach and a system of strong types, pure functions, to formally verify the correctness of a particular ISA. The emulator is nothing more than a side effect.