> success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages.
Dialyzer, the optional static typing system that is of part of the Erlang distribution, is based on success typing. Here is an accessible introduction: