4 ms·

That runtime system is huge. I remember it was an obstacle to high-assurance in Haskell. Is there a detailed write-up on what those 80,000loc do? Maybe someone

That runtime system is huge. I remember it was an obstacle to high-assurance in Haskell. Is there a detailed write-up on what those 80,000loc do? Maybe someone could redo it in one of the verifying, imperative languages like SPARK or ATS to increase its assurance without full verification.

TheAsprngHacker 8y ago
For information about GHC's internals, I recommend reading https://ghc.haskell.org/trac/ghc https://ghc.haskell.org/trac/ghc. The RTS documentation is at https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts.
- nickpsecurity 8y ago
  Thanks!
  - carterschonwald 8y ago
    The rts is pretty nicely written c code. And folks on the ghc irc channel on frenode and mailing lists are all pretty helpful when you have solid questions
noncoml 8y ago
Do you know does it compare to JVM, v8, BEAM, etc? How many locs are they?
- deleted 8y ago
  [deleted]
- lalaithion 8y ago
  HotSpot has ~250,000 lines of C/C++.
carterschonwald 8y ago
Joachim Breitner did a simple high assurances rts backend a year or two ago
Tehnix 8y ago
You might find https://www.aosabook.org/en/ghc.html https://www.aosabook.org/en/ghc.html interesting, which gives an overview of GHC and the decisions they made around it. I haven't heard anything about obstacles for high assurance, but the runtime is definitely considered stable, and rarely needs any components updated AFAIK.
snaky 8y ago
That's doubtful that high-assurance Haskell is in much demand actually. People usually prefer much more strict (in both senses) languages for that, CakeML in particular comes to mind.
- carterschonwald 8y ago
  I tried to figure out what subset of sml cake uses but wasn’t able to find that anywhere in their docs But yeah, it’s definitely true that high assurance / high quality tools are still in their relative infancy (there’s lots of great stuff, but nothing I’d be comfortable using with colleagues at the drop of a hat for a quick project next week)
- snaky 8y ago
  By the way, there is a project to "Implement a front-end for CakeML that accepts OCaml or Haskell syntax" > An involved version of this project would be to write a new verified parser for an alternative syntax. A simpler version would be to re-target the parser in the OCaml compiler to produce CakeML abstract syntax, and treat this as an executable specification. Similarly for any Haskell compiler that is amenable to such treatment. https://cakeml.org/projects https://cakeml.org/projects

TheAsprngHacker 8y ago

For information about GHC's internals, I recommend reading https://ghc.haskell.org/trac/ghc https://ghc.haskell.org/trac/ghc. The RTS documentation is at https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts.

nickpsecurity 8y ago
Thanks!
- carterschonwald 8y ago
  The rts is pretty nicely written c code. And folks on the ghc irc channel on frenode and mailing lists are all pretty helpful when you have solid questions

noncoml 8y ago

Do you know does it compare to JVM, v8, BEAM, etc? How many locs are they?

deleted 8y ago
[deleted]
lalaithion 8y ago
HotSpot has ~250,000 lines of C/C++.

carterschonwald 8y ago

Joachim Breitner did a simple high assurances rts backend a year or two ago

Tehnix 8y ago

You might find https://www.aosabook.org/en/ghc.html https://www.aosabook.org/en/ghc.html interesting, which gives an overview of GHC and the decisions they made around it. I haven't heard anything about obstacles for high assurance, but the runtime is definitely considered stable, and rarely needs any components updated AFAIK.

snaky 8y ago

That's doubtful that high-assurance Haskell is in much demand actually. People usually prefer much more strict (in both senses) languages for that, CakeML in particular comes to mind.

carterschonwald 8y ago
I tried to figure out what subset of sml cake uses but wasn’t able to find that anywhere in their docs But yeah, it’s definitely true that high assurance / high quality tools are still in their relative infancy (there’s lots of great stuff, but nothing I’d be comfortable using with colleagues at the drop of a hat for a quick project next week)
snaky 8y ago
By the way, there is a project to "Implement a front-end for CakeML that accepts OCaml or Haskell syntax" > An involved version of this project would be to write a new verified parser for an alternative syntax. A simpler version would be to re-target the parser in the OCaml compiler to produce CakeML abstract syntax, and treat this as an executable specification. Similarly for any Haskell compiler that is amenable to such treatment. https://cakeml.org/projects https://cakeml.org/projects