Wherein I will gently and briefly guide the reader through certain high-level aspects of the type systems of several programming languages, with the intent to demonstrate that a sufficiently strong and expressive type system can be a powerful tool not only for proving the correctness of our programs, but also for assisting and guiding us in the process of the design and implementation of the programs that we write.