Or maybe the original developer who wrote the code which was so poorly written that it needed 4 paragraphs of explanation did a shitty job. Period. They need to be told to go back and fix it. You see! You argument works both ways, yay!
If the comments are completely redundant with the code, they're bad. But you can't express as code why the some code is the way it is, and why it does what it does. After you tried to express in code every important information that's expressible as code, whatever important information remains must go into comments.
False dichotomy. You are trying to make this black or white while there are many more options beside comments. There are even obvious ones beside comments.
You could. It is called an automated theorem prover, with the cheap limited version called constraint based programming. Sadly very unavailable for most programming languages.
Sometimes writing the proof of why it should be like this is tricky, especially when complexity or performance is involved. (But then the tests are hard too.)
Linters are essentially constraint systems for code, but not for the program.
Theorem provers can still only talk about what the code does and whether or not it does it correctly. Specifying why the code is there is an AI-complete problem. Hence, comments.
