I like the slides and agree with the widening language gap. I have a few comments about the conclusions, though. > The UPenn dependently typed Haskell > progra

I like the slides and agree with the widening language gap. I have a few comments about the conclusions, though. > The UPenn dependently typed Haskell > program shows a great deal of promise and > is likely to manifest a decade before other > DT languages generate practical backends. I don't agree with this at all. The design problems with tacking on dependent types to an existing system are massive - it's a research problem for a reason. On the other hand, writing a "ghc quality" backend for Coq/Agda/Idris/F* seems difficult, but at least it's an engineering problem instead of a rough idea. In particular, CertiCoq is a compiler for Coq written in Coq, and the main problem here is verification. Simply writing a compiler is no harder than writing a compiler in any language. > Interesting ideas out of Microsoft Research on SMT solver > directed programming editors that enforce invariants and can > generate code during development. Another interesting Microsoft Research project along the same lines as Dafny is F. Both are nice, but F is closer to modern dependently typed languages. > Lots of non-local reporting problems associated > with using unification during type-checker. I would argue that the problem is that we use constraint solving for type checking. For example, strict bidirectional type checking leads to more tractable errors, since it's straightforward to follow the compiler's reasoning. On the other hand, bidirectional type checking is less powerful, so it's not like there's a silver bullet here. > Type-safe OTP. I wish more people were working on things like this. There's some theoretical work on calculi for distributed systems, but once they encounter the real world they inevitably become horrendously complicated.