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.