A powerful tool to write proofs by reflection in Coq.
You write everything in Coq. No need to learn a new language. But effects and non-termination are allowed.
You have in hands the full type-system of Coq. You can verify partial correctness properties of your algorithms.
Procedures are extracted to OCaml. Complex results are computed with full speed.