This means type systems help you make your program correct, I agree.

Your argument was "type systems make your programs correct", I still disagree with that.

I think the distinction is important enough.