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
I'm not a mathematician, but I feel the "syntethic"/"analythic" distinction in mathematics is an interesting and useful concept.
"In modern mathematics, an analytic theory is one whose basic objects are defined in some other theory, whereas a synthetic theory is one whose basic objects are undefined terms given meaning by rules and axioms"—Michael Shulman
In programming terms, I guess "synthetic" mathematics feels a bit like programming to an abstract interface.
I didn't read it as a complaint, more of a humorous observation. Either way, there's no need to get aggressive onto someone that hasn't figured it out yet.
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...