Nobody's comparing the aesthetics of sets to types. That's not the point... People want mathematical proofs to automatically determine programs, or to be more t

Nobody's comparing the aesthetics of sets to types. That's not the point... People want mathematical proofs to automatically determine programs, or to be more than just proofs somehow. They want to exploit the capabilities of constructive logic. The fact that arbitrary sets can intersect each other makes extracting computational meaning from set theory proofs harder. The fact that types can be like sets but don't have to be is also why they're interesting: The notion has more flexibility.