Great, but anybody who says correctness is the point of types has completely failed to understand what types are for. Good types do work for you, so that you d

Great, but anybody who says correctness is the point of types has completely failed to understand what types are for. Good types do work for you, so that you don't need to write the code to do that work. Correctness is a side effect, because being wrong would take more work.