I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical t

I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical to write down, but not at all interesting from a research perspective. I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).