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 wri

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