I get the OP’s point: it doesn’t matter what you think about usefulness of knowing how to formally prove anything, the point is that you’re doing it every time you program a computer, so might as well 1) be aware of that 2) learn a thing or two about how it’s done by pros.
Should I study knot theory to tie my shoelaces? Should tailors and cup-makers study topology? Should it be mandatory to study economics before buying groceries?
Looking at code as applied formal logic is not a useful view outside of some rather obscure communities. Even code as a recipe is more useful view in practice.
I’m not saying you should get a phd in logic. I’m saying knowing what your inputs and outputs are supposed to be and writing test assertions is basically checking whether your theorem/lemma is true in disguise (unit of code works as expected) and knowing a bit of theory from that domain can’t hurt. Even if it’s only de Morgan’s laws, which you’ll admit is a rather low bar…
> writing test assertions is basically checking whether your theorem/lemma is true in disguise
But that is almost the polar opposite of treating a program as applied logic. If there is one thing that is not reasonable when dealing with logic, it is "proof by multiple test cases that seem to work, I think".
And I don't clear the low bar for de Morgan’s laws, I've completely forgotten what they are. And on looking them up, that doesn't look like an important component of programming. A programmer could reasonably get away with not knowing them. Probably going to learn them by rote over a few years, but that is hardly "applied logic" in any sense that is worth talking about.
If we could strip out of reality the bits that can be understood as a practical application of the basic branches of math there wouldn't be anything left. Nevertheless most people get a long way in life without needing to engage with that (which is lucky because there is too much to learn in one lifetime).