[baq]

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.

[roenxi]

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.

[baq]

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…

[roenxi]

> 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.