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.