There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants in order to capture in the types important invariants of the program. This allows type-based program verification and is a promising compromise between plain old types and full blown Hoare logic proofs.