Types correspond to propositions in formal logic, and programs satisfying that type are proofs of those theorems. This is called the Curry-Howard Correspondence.

That might not sound particularly interesting, but here’s one of the ramifications: if you need to prove that your program follows some spec for eg avionics software or reactor control software, then one tack is to encode that protocol/spec in a type (usually an extremely expressive type system called a “dependent type” system) then you can prove a program correct to that spec and generate a program that is correct by construction.

This has been done. There’s a C compiler called CompCert where the optimization passes have been proven to not alter the meaning of the program. A tool called CSmith was used to fuzz gcc, clang, and CompCert and found dozens of bugs—but none in CompCert.