Luckily most everyday programs are typeable.
And you don't need cut in logic either: https://philpapers.org/rec/BOODEC
It's just that your typeable program might take more data to store than there are bits in the universe.
I'm not saying that types are bad. They aren't.
I'm saying they aren't magic and they come with a trade off.
alt Hacker News
And you don't need cut in logic either: https://philpapers.org/rec/BOODEC
It's just that your typeable program might take more data to store than there are bits in the universe.
I'm not saying that types are bad. They aren't.
I'm saying they aren't magic and they come with a trade off.