Nice example. For teaching, I like to use this small variation of it, relying on the classical duality between between && and ||. The idea is to state that what you want is that it’s impossible for a to be administrator without activating 2FA. Said otherwise, you want !(Admin(a) && !2FA(A)), that is !Admin(a) || 2FA(a). Which is how we define Admin(a) => 2FA(a).

I haven’t tried teaching implication so I don’t know if this is helpful, but I feel like I can visualize it easiest in terms of modus ponens and modus tollens, pushing truth with the arrow and falsehood against the arrow. Though most of the time I end up looking at it as !A || B.

The “Locked doors, headaches, and intellectual need” article is interesting. It nicely explains why the Metroidvania structure is so effective, building up a tension with inaccessible areas that you’re eager to return to when you gain new traversal powers. I mean to use this for a programming game: there should be a lot of opportunity for the player to realize they have a repeated problem to solve, then the game can either provide an abstraction or encourage the player to build it.

Nice example. For teaching, I like to use this small variation of it, relying on the classical duality between between

`&&`

and`||`

. The idea is to state that what you want is that it’s impossible for`a`

to be administrator without activating 2FA. Said otherwise, you want`!(Admin(a) && !2FA(A))`

, that is`!Admin(a) || 2FA(a)`

. Which is how we define`Admin(a) => 2FA(a)`

.I haven’t tried teaching implication so I don’t know if this is helpful, but I feel like I can visualize it easiest in terms of modus ponens and modus tollens, pushing truth with the arrow and falsehood against the arrow. Though most of the time I end up looking at it as

`!A || B`

.The “Locked doors, headaches, and intellectual need” article is interesting. It nicely explains why the Metroidvania structure is so effective, building up a tension with inaccessible areas that you’re eager to return to when you gain new traversal powers. I mean to use this for a programming game: there should be a lot of opportunity for the player to realize they have a repeated problem to solve, then the game can either provide an abstraction or encourage the player to build it.