Post #4287325

re: examples (https://hci.social/@chrisamaphone/117004836285009044) when i meet a new-to-me logic or type theory, it's like someone has just handed me a phrasebook for a language i don't yet speak. the beauty of it is it gives me a new vocabulary in which to ask questions. example: when meeting linear logic, one can ask, "is [A & B ⊸ A ⊗ B] a theorem?" & the theory can answer. i eventually want to study properties of the theory from outside, but i build all my intuition from conversing with the theory in its own language.