Their process was extremely elaborate. They wrote a Haskell prototype which was then automatically translated to their specification/verification language (Isabelle/HOL). They then proved all the theorems they wanted (which, I can only guess, was very hard), and hand-translated the spec into C. Then they proved that the C translation was a refinement of the spec (i.e. doesn't deviate from its boundaries) using a theorem prover and an SMT solver.
That last part (translation validation[1]) is what I found most interesting, or, at least, the most novel. Here's the paper: http://www.cl.cam.ac.uk/~mom22/pldi13.pdf
That last part (translation validation[1]) is what I found most interesting, or, at least, the most novel. Here's the paper: http://www.cl.cam.ac.uk/~mom22/pldi13.pdf
[1]: http://download.springer.com/static/pdf/209/chp%253A10.1007%...