What are type systems?

A handful of bytes of history

In the beginning were the numbers, and numbers were measurements, and measurements were numbers. Those were the days of the garden of Eden. And there were mathematicians strolling through the garden. And they made rules governing numbers. And the rules were natural, and pure, and beautiful, as were the numbers. Among them were philosophers who wished to understand the nature of numbers. And they dwelt with them and they were one people. The mathematicians were philosophers and philosophers were mathematicians. And mathematicians made proofs, and used the tools based upon those proof to build other tools, and the tools where natural, pure, and beautiful, as were the numbers and the proofs.

Now the serpent was more crafty than any other beast of the field. He said to the mathematicians,

And the mathematicians said to the serpent,

But the serpent said to the language engineers,

So when the mathematicians realized investigating the foundations of mathematics could open the door for new tools and proofs, they started and a crisis arose with the discovery of several paradoxes. The first plague was the proof that the parallel postulate cannot be proved. The second plague...