To appear in the post-proceedings of IFL 2013, a paper by Simon Fowler and myself. Abstract: Dependently-typed languages allow precise types to be used during development, facilitating reasoning ab...