It's really not the honor system. If you verify with a type checker, you are proving that various type errors are impossible, provided that the caller respects

It's really not the honor system. If you verify with a type checker, you are proving that various type errors are impossible, provided that the caller respects the type system. The rigor is exactly the same, it's just that the type system allows for "gradual typing" so that it doesn't need to be strict as in a fully-typed language.