> And in theory, dependent types are the awesomest thing ever. But they're not ready yet, and there's no guarantee they ever will be. I think the reason depend

> And in theory, dependent types are the awesomest thing ever. But they're not ready yet, and there's no guarantee they ever will be. I think the reason dependent types haven't made it into practical programming has less to do with them being not ready and more to do with them being fundamentally challenging to learn. I have a pretty strong pure math background and it still took me a significant amount of time to wrap my head around them to the point that I could write non-trivial proofs using them, let alone programs. For programmers who have never done much formal logic or who have never heard of a category, I can't imagine how much time it would take to get the prerequisite knowledge. Another issue is the fundamental problem of creating a new language; you have to build up a ton of extra machinery (libraries, tooling, etc.) to even think about it becoming more than a toy, even if you don't care about it being mainstream. Rust has the backing of a large open-source company and a ton of really smart people dedicated to bringing it to primetime, but it is still going to take a long time for it to get there. Dependently typed languages like F* and Idris don't have the same manpower behind them and also have to face fundamental challenges like integrating formally verified code with a world full of unverified (but useful) code.