Awesome research from Microsoft

actual title: "Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq"

All this coq 'n agda stuff won't produce anything of practical value to software engineering before the singularity arrives. Haskell is already too much for practical work, ocaml's near the perfect typed language point.