> To some degree, you can choose what you want to prove about your algorithms in those languages.
> It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.
Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).
Also, consider how when you start making use of generics in type systems by converting all you Object lists to String lists; you find you have to start adding generic types all over the place for any code that touches that code until the compiler errors stop. If you decided to capture permutations of input lists in a dependently typed language, the exact same thing happens except this time capturing that property for all your algorithms could be monumental task of writing complex proofs (unlike before where you're just labelling things).
> Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).
So don't write the proofs then. Dependently typed languages don't require you to write proofs; they give you the ability to if you choose. Considering that it's impossible to write such proofs in OCaml or Haskell, it seems strange to complain that they're hard to write in a dependently typed language. "Hard" is strictly less difficult than "impossible".
> Considering that it's impossible to write such proofs in OCaml or Haskell, it seems strange to complain that they're hard to write in a dependently typed language.
My sole point is that when I see articles on here about dependently typed languages, the issue of how the proofs are generated and the challenges involved in doing this is overlooked almost every time. I think it's important these challenges are highlighted so people don't think dependent types are a magic wand that gives you safety with little effort.
The article was talking about the differences in power between different type systems. It's not even primarily focused on dependent types, let alone advocating for using them or claiming that they're easy. In fact it notes that the more advanced type systems "make the language more complex." If the article were suggesting everyone should use dependent types, or that they were easy, then your admonishments about dependent type systems would make sense here, but as it is I'm not sure.
Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).
Also, consider how when you start making use of generics in type systems by converting all you Object lists to String lists; you find you have to start adding generic types all over the place for any code that touches that code until the compiler errors stop. If you decided to capture permutations of input lists in a dependently typed language, the exact same thing happens except this time capturing that property for all your algorithms could be monumental task of writing complex proofs (unlike before where you're just labelling things).