I'm a bit skeptical about logic being engrained in human thinking. Sure, we might understand "or" from childhood, but what about the distinction between inclusive and exclusive or? It seems this is naturally glossed over, and making a clear distinction has to be taught.
I also wonder about nesting and scopes. I'm reminded of a blog post I read [1] where subtleties of generic and existential types in Rust are explained using the scopes of the for-all and there-exists operators in the equivalent logic. On the one hand, this is a helpful clarification. But understanding nested logical operators doesn't itself seem all that intuitive or natural?
Intuitive everyday logic does
work a bit different
This is true.
Intuitive everyday logic does work a bit different in most people from propositional and first-order logic, in particular with regards to or and implies. For example, most people's or is the exclusive or you mention. But both logics can explain each other. For example, not, and as well as for all is pretty similar in formal and informal logic, and, as you know, those three are a basis for all of (first order) logic.
I also wonder about nesting and scopes. I'm reminded of a blog post I read [1] where subtleties of generic and existential types in Rust are explained using the scopes of the for-all and there-exists operators in the equivalent logic. On the one hand, this is a helpful clarification. But understanding nested logical operators doesn't itself seem all that intuitive or natural?
[1] https://varkor.github.io/blog/2018/07/03/existential-types-i...