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.