>Types can prove that certain inputs can never be received by a piece of code, which is a stronger guarantee. I'd amend this to say that sometimes the compiler

>Types can prove that certain inputs can never be received by a piece of code, which is a stronger guarantee. I'd amend this to say that sometimes the compiler can prove you're calling a function with or setting a variable to an incorrectly-typed input, but at runtime a strong type system by itself doesn't prevent receiving those inputs, only executing them. It is possible to create a programming language with semantics such that the compiler will always catch incorrectly-typed inputs, but that's a separate but related concept from the type system.