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.
Haskell is already too much for practical work?
No.
I use it as my main scripting language.
Have you tried ocaml. Haskell keeps moving, takes much longer to get to grips with, and most users don't use all it's features (which keep growing). Meanwhile you can get your head around all of ocaml pretty easily and it gives you no surprises. Ocaml is for coders, haskell's for grad students.
I haven't tried it, but sounds like I should :)
Yea, along with prolog, it's one of the hidden pearls of programming
This paper may not be singularity stuff, but it is from January 2012!
this formal methods shit has been going for decades and will do so for decades more being hardly used by anyone, by which time the singularity will arrive and nobody will need to program