> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that
You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to.
I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`.
I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself.
There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write.
BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.
Yes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this:
app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil ys = ys
app (x :: xs) ys = x :: app xs ys
You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to.
I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`.
I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself.
There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write.
BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.