What are types? What can we do? What do they denote and represent?
Types denote functionalities, that is functional behaviours. There are two flavours of types, there are the implicit types, there are really predicates or sum sets of the domain of this course.
Or they can be explicit, in the sense that they denote domain and co-domain of functions.
There are not really sets, although one can think that types can behave as sets, because sets naturally carry with them a sort of cumulative notion, while types keep the layers always separate.
But both of all types are useful because they can represent propositions in a constructive logic. This is perhaps one of the reasons why typed l-calculus is so successful in this sort of area. Well, typed l-calculus calculus is a very good language for the note in proofs and - as I said - proofs, formal proofs, proofs and formal systems are the basic ingredient for formal methods.
They can also represent, when you use type theories as metamodels, they can represent judgements in logic.