what is the substance of this complaint?
if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works.
let me translate for you:
proof assistant: program that checks your work (writing a proof) and helps you find new proofs.
synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects)
1-category: a collection with objects and functions between them
2-category: a collection with objects, functions between them, and functions between those functions (called homotopies)
k-category: you get the idea
∞-category: the limit as k -> ∞
second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff
and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...
if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works.
let me translate for you:
proof assistant: program that checks your work (writing a proof) and helps you find new proofs.
synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects)
1-category: a collection with objects and functions between them
2-category: a collection with objects, functions between them, and functions between those functions (called homotopies)
k-category: you get the idea
∞-category: the limit as k -> ∞
second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff
and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...