SETS VERSUS TYPES
ORIGIN
SETS are a part of mathematics designed for formalization and
consistency proofs.
In order to show that something can exist, program it in set theory!
Therefore set theory is no typical math: You don't ask for structure
up to isomorphism but for a concrete implementation.
TYPES were invented to solve fundamental consistency problems
by restricting set formation. Today, it seems that
there are better solutions for this.
USAGE
In absence of a better standard,
mathematicians use a the common part of many different SET theories
as their common meta-language. This works quite well for our times.
Some computer scientists abuse set theory for specification (Z),
which is a pity.
TYPES are enhancing specification and computer-assisted mathematics
like proof checking and automated theorem proving. Since types do a
great job here, some people think that they would also be suited
for a future mathematical meta-language.
In computer science, strongly typed languages are a great help in
decting many bugs at compile instead of run time, which is of great
economic importance.
In functional programming languages like ML,
the strong typing becomes even more useful because
there the types are relevant also for the control structure.
Therefore, in ML the compiler can automatically detect practically any bugs
in a program that result from the programmer writing a program
that is different from the program he has in mind.