Thank you so much for that second link! I've been interested recently in how dependently typed languages can be made more natural for general-purpose programming, and this looks like a really good read. It gives me hope that it won't be too long before there's a dependently typed language comparable to Haskell in terms of community and ecosystem - in my (limited) experience, Agda and Idris are awesome for theorem proving and for small programs, but they're both a ways off from being usable for large, complex programs, and I feel like a big part of what they're lacking is just well-documented libraries for common operations.