4 ms·
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 pa
by 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 agoI 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 agoBy 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