3 ms·
As for dependent types, it's probably just that the type systems for them are simply not yet mature enough to be practical for most tasks.
by continuational 9y ago
As for dependent types, it's probably just that the type systems for them are simply not yet mature enough to be practical for most tasks.
- seanwilson 9y agoIf you're using a dependently typed language, you have to write maths proofs to prove properties hold. It's incredibly challenging and not going to be automated any time soon.
- agentultra 9y agoI think that's going to change. It's my completely biased, uninformed opinion that dependently typed systems are much easier to reason about than their counterparts.