How is a type system related to a progam?
Your understanding that a type system is a set of rules in a formal system is right, but the rest is a bit garbled.  The purpose of the type system is to delineate which terms or programs make sense.  It is up to the language designer to decide which programs "make sense".  There is no claim that the language specifies all programs that make sense.  When somebody proposes a new type system, they are saying, "here are more programs that make sense and our type system captures them."

Andrej is saying one shouldn't equate the type system with the type checker (which is a program).

There is nothing too deep about it.  Merely that the type system, i.e., the set of rules, stand independently of any particular implementation.  One could even devise type systems that are undecidable, i.e., no possible type checking program exists.  Admittedly such type systems may not be of much practical use, but nobody denies that they are type systems in the first place!