I think we have different definitions of "lazy/sloppy thinker"
Consider someone who regularly formalizes math proofs in Lean / Coq. Can they be a "lazy/sloppy thinker"?
In my definition, no. Anyone that daily battles Lean / Coq to submission is thinking very rigorously and clearly.
If I understand your / @ZiCog's definitions correctly, under your definition, yes -- in fact Lean / Coq is great for lazy/sloppy thinkers because one can be lazy/sloppy, and the compiler will catch all the errors.
If we replace Lean/Coq with rustc, this seems to be the two sides of the argument.
I don't think either of us will convince the other of the "correct" definition, but it seems our disagreement stems from having different axioms / definitions.