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