> There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in type definitions and you can have bugs in tes

> There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in type definitions and you can have bugs in tests as well and that'll be a problem until computers can read our minds. Type definitions are superior at checking what you specified though because the checking is exhaustive. Perfect is the enemy of good and all that. > This is no different from writing tests in a dynamic language. It's not. In that example, the type system will verify the stated property is true for all values of "s". Tests only check some specific examples whereas using types in this way tests all possible input and output pairs. It's like comparing a maths proof to checking an equation holds for a few examples you tried.