[pron]

OK, so `id` is basically syntax (or access to the meta-language) for a schema. Thanks for explaining that! In Lean you can certainly feel this sometimes, as you can't even write the proposition `id = id` or `id id = id`. I guess there is no escaping such mechanisms in consistent formalisms, but I've found myself running against such subtleties much more often in Lean than in TLA+, and certainly far sooner (giving me a persistent feeling that I don't really get it). For example, the entire universe hierarchy is something to be aware of from the start (even though Prop is exempted from it), and is completely accidental complexity (necessitated by the chosen formalism, but still) from the perspective of someone just interested in specifying and verifying programs. I think that in most, though not all, cases, TLA+ has a somewhat better story in that regard. For example, definitions parameterized over the domain of the entire universe are syntactically distinct from functions (even in the use-site), and access to the meta-language, required in order to universally quantify over formulas when writing theorems/axioms that serve as inference rules (e.g. well-founded induction), is done in a way that's syntactically distinct from formulas.

When playing with Lean (and I guess the feeling may go away if I ever invest enough time to become proficient in it) I feel like fighting the formalism, which works hard to maintain consistency while having formulas represent "intensional" objects (meaning objects other than true/false), which is a feature that may be very interesting to logicians, but as a practitioner, it feels like paying a high price for something I absolutely don't need. HOL should be simpler, but the Isabelle/HOL tutorials are seriously lacking, and the whole quoting system there is a lot of accidental complexity that I didn't want to bother with.