> Presenting type-level programming as a good thing > Fetishizing Curry-Howard These seem a bit causal :) When you do closer and closer to dependently-typed

> Presenting type-level programming as a good thing > Fetishizing Curry-Howard These seem a bit causal :) When you do closer and closer to dependently-typed programming (which necessitates more type-level programming because dependent types aren't present in any production language yet), Curry-Howard actually can be a nice way to ground yourself when you get confused or stuck programming at the type level.