Software has evolved on a direction where sending sets around is natural. That is no evidence that sending theorems around is problematic, it's just that current communication implementations happens to be very data-friendly and logic-unfriendly.

There is probably a very human reason for that, but mathematically both representations are perfectly replaceable.