> - No type inference, since that's not decidable for dependent types. You can still have type inference, it just won't be able to infer the type of all valid

> - No type inference, since that's not decidable for dependent types. You can still have type inference, it just won't be able to infer the type of all valid terms, in which case you just have to add a manual annotation. This is not a strange concept, this is what haskell does for example with higher ranked types. > getting the specifications is a big problem You do not need to specify what the whole program will do (in fact you can use a language with dependent types without having to specify anything at all) - that being said, people usually specify the behavior of specific functions in the program. > - Relatedly, dependent types don't solve the oracle problem in software engineering: i.e. where do you get the specs from and how do you know that your specs (in this case types) are correct rather than false? I thought that the point of erlang having dependent types would be to make data-dependent code easier, not to specify the behavior of functions. But yes, this is correct, and this holds true with every proof assistant that I am aware, not only with the ones that use dependent types. > because you now also have to rewrite / refactor the specifications This is a great thing actually - I would consider it a bug if my function after a refactoring did something that went against its specification, with dependent types I can have the compiler warn me about it. But again, you are not forced to write a specification. Dependent types only add possibilities without removing anything. > So it's not like programming language designers don't know about them. I would argue that most programming language designers are not familiar with type theory. There are thousands of languages, one does not need to be a genius to make one. Heck, two of the most popular languages (C and Go) do not even have parametric polymorphism, not to mention that generics were added in Java only in 2004. In addition to that pretty much no popular language has proper support for higher order types either. > industrial code, 20k LoCs, at least 3 programmers involved, specification changed over time. Specification was not fully available at the start of the project. In that case, none. Though I would argue that your standards are too high, after all just the fact that I have not worked in the software industry excludes anything that I have made. As for LoC, I would not use it to measure the scale of a project. With Java for example even the most trivial program can easily reach thousands of lines.