The way I look at it is that "types" are assertions, which tell us whether our assumptions about the program are correct or not. There is no such thing as a "co

The way I look at it is that "types" are assertions, which tell us whether our assumptions about the program are correct or not. There is no such thing as a "correct program". There is only our correct or incorrect understanding of what the program is doing. Type-declarations help us gain the understanding about that. Types express data, which allow the assertions to be structured and composite, and express assertions about the real data running through the program when it executes. So "types" in a sense do not exist as such, we are simply writing "predicates" in some formal language. Whether those predicates are checked at compile-time or run-time is a separate question. The reason many people assume that 'types' are a thing is that when using a "statically typed" language you are required to enter them always, and therefore they take on more or less existence of their own. Using a typed programming language you are always writing TWO programs, one that does what you want it to do, and another that observes and verifies the code's adherence to your assumptions about it. Thus types are a secondary utility, they are a harness that limits what your program can do. Types help you to better understand and to gain trust in your understanding of your program.