> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in

> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of I don't want to argue with you on the theory side since I am not an expert, but I can assure you that Idris is a nice language to work with. I prefer haskell due not non-dependently typed stuff, but I think otherwise it clearly shows that a practical dependent programming language to do actual real-world work is possible and ergonomic. EDIT: I also don't think that verification is the main advantage of dependent types. Haskells type-system is already unsound (f:: a -> b, f=unsafeCoerce, the universal proving function). I like it because it makes it easy to express more complicated constraints in an ergonomic and approachable way and therefore make the compiler just accept less programs. I see it as minimizing the chance for stupid bugs and give the programmer more information about what's going on by providing richer types.