4 ms·

Is this subset of F# itself formally specified? How is it different from an emulator that is slightly more clear to read?

davidgrenier 3y ago
My understanding of this is that it is an emulator that is meant to be very clear to read.
- davidgrenier 3y ago
  It isn't though: https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d00e4854e4c721e8ec0dd/CLI.fs#L77 https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d0...
  - genter 3y ago
    As far as F#/OCaml goes, that's excellent. (I'm convinced one of the reasons why Rust is so popular is because it's OCaml with a legible syntax.)
    - pharmakom 3y ago
      F# has diverged quite a lot from OCaml and is very readable IMO. In any case, I think this view stems from our Algol/c/Java centric CS education system that casts ML and Lisp as weird and “unreadable”, when really it’s just a matter of perspective.
      - jcelerier 3y ago
        > when really it’s just a matter of perspective. it's really not, in the engineering school I did in the first year we were taught both C and LISP during the same semester and it was obvious to almost everyone except math nerds how much easier C was mapped to a normal human being (e.g. someone without prior programming experience)'s mental model of the world
  - yazzku 3y ago
    Hadouken! They wish they had monads.
    - phillipcarter 3y ago
      Not necessarily. I would say that the hand-rolled argument parsing business it a call for Argu: http://fsprojects.github.io/Argu/tutorial.html http://fsprojects.github.io/Argu/tutorial.html But the code isn't all that complicated to begin with.
mrLSD-dev 3y ago
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 3y ago
  >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 https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv 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 3y ago
    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 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 3y ago
      >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.

davidgrenier 3y ago

My understanding of this is that it is an emulator that is meant to be very clear to read.

davidgrenier 3y ago
It isn't though: https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d00e4854e4c721e8ec0dd/CLI.fs#L77 https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d0...
- genter 3y ago
  As far as F#/OCaml goes, that's excellent. (I'm convinced one of the reasons why Rust is so popular is because it's OCaml with a legible syntax.)
  - pharmakom 3y ago
    F# has diverged quite a lot from OCaml and is very readable IMO. In any case, I think this view stems from our Algol/c/Java centric CS education system that casts ML and Lisp as weird and “unreadable”, when really it’s just a matter of perspective.
    - jcelerier 3y ago
      > when really it’s just a matter of perspective. it's really not, in the engineering school I did in the first year we were taught both C and LISP during the same semester and it was obvious to almost everyone except math nerds how much easier C was mapped to a normal human being (e.g. someone without prior programming experience)'s mental model of the world
- yazzku 3y ago
  Hadouken! They wish they had monads.
  - phillipcarter 3y ago
    Not necessarily. I would say that the hand-rolled argument parsing business it a call for Argu: http://fsprojects.github.io/Argu/tutorial.html http://fsprojects.github.io/Argu/tutorial.html But the code isn't all that complicated to begin with.

mrLSD-dev 3y ago

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 3y ago
>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 https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv 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 3y ago
  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 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 3y ago
    >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.