The thing about being wrong with types is that the end result is an immediate compiler failure. It can be difficult to figure out the right types, but once you do they're certain to behave properly. Thus, the penalty for wrongness is nearly nothing at all.
You face the infinite amount of wrong by working really hard to understand the right.
If you're wrong in values it'll probably still work for a while until it suddenly doesn't for rather mysterious reasons. This can be way down the line, undetected for a long time if not forever. Thus, the pain of being wrong is potentially infinite as well.
So, programming in types is no easier. It's probably even harder today since so few people do it. But the consequences are amazingly different.
And yeah, with Conor's work its "come for the puns, stay for the mind blowing computer science"
> the penalty for wrongness is nearly nothing at all.
Well, I think Edwin Brady showed a couple of C++-template-errmsg-like-things during a couple of his talks, but having actually programmed semi-advanced C++-template things I think I can agree on the general thrust that type-level problems are in some sense "better problems to have".
Btw, thanks for the exchange. (This is getting too off-topic, so I'll leave it at that.)
You face the infinite amount of wrong by working really hard to understand the right.
If you're wrong in values it'll probably still work for a while until it suddenly doesn't for rather mysterious reasons. This can be way down the line, undetected for a long time if not forever. Thus, the pain of being wrong is potentially infinite as well.
So, programming in types is no easier. It's probably even harder today since so few people do it. But the consequences are amazingly different.
And yeah, with Conor's work its "come for the puns, stay for the mind blowing computer science"