Tock and Filet-O-Fish

The only good compiler is a correct compiler. Can we combine Filet-O-Fish and Tock to write a provably correct occam-pi compiler?

This involves diving into Haskell, the Filet-O-Fish DSL, and ToCK, our experimental compiler for occam-π. Great if you're into formal methods and languages. Not for the faint of heart.