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 forato be administrator without activating 2FA. Said otherwise, you want!(Admin(a) && !2FA(A)), that is!Admin(a) || 2FA(a). Which is how we defineAdmin(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.