Agda and Idris are both very interesting to me, especially the latter since it was designed with systems programming (read: real-world applications) at its core. They both seem kind of like beefed-up Haskell.
However, I wonder how much actual utility they can provide, seeing as (1) dependent typing is generally acknowledged to be rather difficult (and that's a statement coming from those who generally tend to already be good at a language like Haskell), and then also (2) the fact that a great deal of real-world applications, such as FFI, accepting data over a wire, dealing with exceptions and faulty input, etc, mean that no matter how bullet-proof the code you write is, you'll still have to account for all of the ugliness which the world can throw at you, which means unit testing, exception handling and other things which seem to undermine - to a degree - the strengths of strong typing in the first place.
Or am I exaggerating things? I've written a lot in Haskell and enjoy it a great deal, but at work I use Python and JavaScript, and honestly, although there are some things that would be streamlined away by a strong typing system, particularly in the development cycle, there are still a ton of ugly, mundane real-world things that would still need to be dealt with in much the same way if they were written in Haskell. I would still love to have the opportunity to write in Haskell (or Agda or Idris, etc) at work, but I'm not sure how much trouble it would save me from at the end of the day. Would it? And would the additional mental hurdles of dependent typing add real tangible benefits on top of this?
