[mrLSD-dev]

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.

[nullifidian]

>it allows to formally verify the correctness of a particular ISA

That must be hypothetical. "Functionalness" of the language/code doesn't make everything that is written automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.

https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.

Your executable specification could probably be called "Formal", in the same sense as a PDF spec being called "Formal", but being subject to verification by the virtue of F# being functional or being written in the functional style might be pushing it too far.

[mrLSD-dev]

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.

[nullifidian]

>this is not a formal verification

Then what have you meant by "allows to formally verify"?

>Haskell example:

I think (I'm not gonna insist on it) they are misusing the word "formal" too. Formalization must involve logic/math, i.e. a formalism, either in code or in prose. Just having lambda calculus as a base somewhere deep doesn't cut it. Haskell's type system is known to be (logically) unsound/inconsistent for example. This is an executable specification imho.

[mrLSD-dev]

Just out of curiosity, what about that: https://people.csail.mit.edu/bthom/riscv-spec.pdf

[nullifidian]

They chose Haskell for the reasons stated in the section 2.1. Namely human reasons of it being a general purpose language that is supposedly more readable by engineers, and preexistence of translators that they needed. To me the "formal" aspect of their spec starts after the output of the hs-to-coq compiler, which isn't a verified compiler. I already have to trust coq, in which about a paradox a year have been discovered(maybe less now), and which isn't small (about 20k lines minimal core iirc). Trusting an additional compiler and a language subset(some total Haskell subset) is stretching it formality wise. Using a general purpose language is also their innovation (Academic papers sometimes are written to cover the yet unclaimed design space, not necessarily because the approach is the best or practical). They even used the following language "It may turn out that the ideal community-shared spec language is quite different from Haskell, but our interest here is showing that a general-purpose language can work well as the host for a multipurpose spec, leaving fine-tuning of the approach for future work." I see no reason why they couldn't have done it in coq or lean directly, other than the inconvenience(having to write to-verilog and other translators) and "non-innovativeness"(publishability). Good old C today has been fully formally specified, and therefore could also technically be used to provide a "formal" specification for hardware. Would it be a good formal specification? The further it is from the logical core the less useful it seems to me as a formalization. Haskell's formal aspects are also scattered across multiple papers throughout the years and Haskell's versions as far as I know. Coq on the other hand has https://github.com/MetaCoq/metacoq

[trealira]

> To me the "formal" aspect of their spec starts after the output of the hs-to-coq compiler, which isn't a verified compiler. I already have to trust coq, in which about a paradox a year have been discovered(maybe less now), and which isn't small (about 20k lines minimal core iirc). Trusting an additional compiler and a language subset(some total Haskell subset) is stretching it formality wise.

I'm a bit confused from my lack of knowledge here. If it's fed into Coq, why does the origin of the code matter? As it's a proof assistant, wouldn't it reject invalid proofs of validity (assuming you fully trust Coq)? Shouldn't it be fine even if the code is randomly generated by monkeys on typewriters?