[Gajurgensen]

If I recall correctly, most CakeML code is actually written in HOL4 and then translated down to CakeML, and compiled to machine code from there. Unfortunately there isn't very much in the way of documentation or examples for writing concrete CakeML, as the developers seem to use it more as an intermediate representation.

Edit: The page describes two frontends. The first is a "proof-producing synthesis" of a CakeML AST from "ML-like functions in HOL". This is what I believe is the more typical use case of CakeML. The second frontend is a more traditional frontend which parse concrete CakeML syntax.