3 ms·
Awesome research from Microsoft
- mukyu 15y agoactual title: "Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq"
- marshallp 15y agoAll 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.
- BasDirks 15y agoHaskell is already too much for practical work? No. I use it as my main scripting language.
- marshallp 15y agoHave 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.
- gtani 15y agoThis paper may not be singularity stuff, but it is from January 2012!
- marshallp 15y agothis 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