[godelski]

As someone who came over from physics to CS this has always been one of the weirdest aspects of CS to me. That CS people believe that testing code (observing output) is sufficient to assume code correctness. You'd be laughed at in most hard sciences for doing this. I mean you can even ask the mathematicians, and there's a clear reason why proofs by contradiction are so powerful. But proof through empirical analysis is like saying "we haven't found a proof by contradiction, therefore it is true."

It seems that if this was true that formal verification should be performed much more frequently. No doubt would this be cheaper than hiring pen testers, paying out bug bounties, or incurring the costs of getting hacked (even more so getting unknowingly hacked). It also seems to reason that the NSA would have a pretty straight forward job: grab source code, run verification, exploit flaws, repeat the process as momentum is in your favor.

That should be easy to reason through even if you don't really know the formal verification process. We are constantly bombarded with evidence that testing isn't sufficient. This is why it's been so weird for me, because it's talked about in schooling and you can't program without running into this. So why has it been such a difficult lesson to learn?

[snovv_crash]

The fact that a lot of code doesn't even have tests, and that a lot of people don't think even writing tests is a good thing, should shock you even more.

[godelski]

I teach so I'm not too shocked lol. But there's a big difference between beginners doing this and junior devs. But the amount of Sr devs doing this shit and not even understanding the limits of testing, well... a bit more shameful than surprising if you ask me