F# RISC-V Instruction Set Formal Specification | Hacker News Reader

F# RISC-V Instruction Set Formal Specification

github.com

122 pointsadamnemecek16 comments

To me "formal specification" sounds like it should have some sort of connection to formal methods, i.e., some proof system. This looks more like what I would call an "instruction set simulator". Though if the focus is on clarity and readability rather than performance, "executable specification" might be a good middle ground.

In this context "formal" just means that no parts are left open to interpretation [1]. While proof systems are definitely formal that implication doesn't work the other way around.

Under normal circumstances programming code is unambiguous and should therefore suffice as a formal definition / specification (with most programming errors stemming from the fact that this formal definition doesn't match the informal definition the programmer or customer had in mind).

[1]: For comparison, https://en.wiktionary.org/wiki/formal defines 'formal' as: "(mathematics) Relating to mere manipulation and construction of strings of symbols, without regard to their meaning".

> In this context "formal" just means that no parts are left open to interpretation

Yes. But as you say, by that token any instruction set simulator could be called a "formal specification" (modulo undefined behavior, or if you deliberately wrote in a language with nondeterminism). But we don't call them that, because (I maintain) there is something more to being a "formal specification". Namely, being in a form that is easily amenable to formal methods tools, and the intention to apply these tools.

Now of course a pure F# or Haskell program is much closer than C to being analyzed by formal methods tools, but there is still a gap that wouldn't be there if the specification were written directly in Coq or Agda or Isabelle or whatever.

The main reason code isn't considered a formal specification is that it's not intended to be either formal or a specification. That doesn't mean you cannot write a formal specification in code.

If anything code allows for a higher level of formality than all but the most formal mathematics. Which is why some mathematicians are advocating that mathematical proofs should be specified as code [1]. You shouldn't confuse the existence of these languages to mean that any code not capable of expressing mathematical proofs is not formal. It might be limited, but not informal.

[1]: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

It's the first step in a lot of formal methods. Like proving an implementation's adherence to the model requires a machine readable model. Or proving certain aspects about the model.

For instance part of sel4's proof chain is a machine readable model of an ARM. It then uses that to prove equivalence of the generated binary to the high level spec of the kernel.

Here is one in Haskell which is more complete: https://github.com/mit-plv/riscv-semantics. For example, it supports 64-bit ISA while this one doesn't yet.

Maybe it could be ported to SML, because:

> "It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997)."

https://en.wikipedia.org/wiki/Standard_ML

edit, the specification itself: http://sml-family.org/sml97-defn.pdf

There are multiple WIP formal specs for Risc-V it seems one will be chosen as official and is then likely to be used for further tooling eg hardware and software verification.

Coming from a different background, I wonder what this project tries to achieve? And why F#?

What other language? Haskal is too much, Python is too little, Rust is essentially F#.

Could you elaborate on why something like Haskell is too much? Similarly, why is Python too little?

Python gives you too little in terms of formal verification. Haskell is hard to map to other langs.

Why not f#? I would imagine it has good support for discrimated unions which are quite good for representing instruction sets.

He wanted a more modern platform than ocaml, or ml. He didn't want to go too deep down into the functional rabbit hole(haskell), and he didn't want to think about memory management at all(rust).

I find it strange that this comment is downvoted, while being only comment here asking "what does it do". As far as I understand this can be used as emulator of RISC-V processor. It is also has very verbose and clear code, so one can learn RISC-V instruction set reading it. It is specification written in programming language, which is a good reference. I find it easier to read than documentation, for example.

F# is because it's as good programming language as any.

Thanks, that was the only usable answer.

Would make up a great blog post, about highlighting the weaknesses and strength of F#, if there are any?

Reply on news.ycombinator.com