A Haskell Compiler – Slides on GHC Implementation (2013)
scs.stanford.edu
scs.stanford.edu
I haven't heard anything about obstacles for high assurance, but the runtime is definitely considered stable, and rarely needs any components updated AFAIK.
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)
> 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.