2026-07-29 16:14 UTC
Replies (2)
-
@carloangiuli@mathstodon.xyz 2026-07-29 16:37
@chrisamaphone@hci.social Btw, my take on this -- and on the original case -- is just that it's a human question of what concepts we can wrap our heads around despite being formally incredibly complicated. Obviously that varies by person and by experience, but I actually worry that formalization allows us to get too far ahead of our skis sometimes. I also *do* think dependent type theory is very complicated, although I also think there are many principles at work that compress it considerably. And for what it's worth, inductive schemas and pattern matching scare me most of all! I was just asking Mario and @mevenlennonbertrand@lipn.info about them last week...
-
@chrisamaphone@hci.social 2026-07-29 18:05
@carloangiuli@mathstodon.xyz "know how to elaborate to" is doing some work here. i don't need to be able to fit the entire tech tree of definitions in my head at once, but i should be able to reduce the top layer down to previously-understood mathematical principles (whose definitions in terms of foundations i could reconstruct if i put in the time). and yes, of course this is subjective; trust is a social construct