Type checking relation to logic
https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ - This book.  

A type for a parameter is like a precondition, and a type for a return value is like a postcondition.  Structs function as an AND operator, and Unions function as an OR operator.  When you say

performTransaction(x : DollarAmount) : Result

If x had to be constructed as a valid DollarAmount type, then this function is only callable if that was possible.  Also, the Result type is guaranteed to have some fields on it (error codes, transaction id, etc); and performTransaction has to construct the object to give it to you.  So, if you view statements like "x : int" as "x is proven to be an integer", then it is not a stretch to have something more elaborate like:  " x : int, x > 0, x &lt; MAXINTEGER " to assert that x is a positive integer (a DependentType is a type that depends on the value, typically notNull, notZero, etc).

You can make functions take in very specific types that indicate an initial state, and return new types that indicate new states; and use types to enforce constraints on following a state machine - at compile time in many cases.