[Sharlin]

Types constitute this sort of a partial proof. Not enough to encode proofs of most runtime invariants (outside powerful dependent type systems) but the subset that they can encode is extremely useful.