>It is based on dependent products which you need to understand sooner-or-later (sooner, really),

Type-theoretic universal quantification _is_ the dependent product (/dependent function, a term I prefer). I assume you're talking about the Cartesian representation, but that's just one way to visualize it, the definition is not dependent on it. If you understand predicate logical quantification it's not necessary at all, since the introduction/elimination rules for type theoretic quantification are the same as for normal predicate logic quantifiers.

>are rather more intricate than FOL

Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say.

> Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory).

Why would it not be a function? With set theory you have the issue that you can't take a set as an argument and have the codomain and it's elements be dependent on it, but that's exactly what dependent function types allow you to do. The universe U is a sort and A is a valid sort too, so

forall A:U. forall a : A. A

is a perfectly valid function signature and the term would just be (lambda A : U. lambda a : A. a). That doesn't strike me as any more complicated than your second TLA+ example. Sure, you have to deal with universe polymorphism, but I'd say that's compensated by the increased complexity from having to use syntactic operator.

Lean's syntax to specify the universe U is admittedly pretty ugly, but the actual meta-theory isn't that complex I'd say.

> Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say.

It's not that. It's hard for me to try and quantify some essential complexity of a type theory and a set theory, but programmers don't usually learn type theory in high-school or college, but FOL comes "for free" (not to mention the unnecessary complication of constructive mathematics with special handling of noncomputable functions for specifying digital systems) and engineers don't even need to learn the inference rules, because they will rarely bother writing proofs; just pressing the button on the model checker has a much better cost/benefit, plus it allows learning just semantics first, even you do want to learn deduction later. With TLA+ there isn't much to grasp or learn; you know most of the basics. It could just be a situational thing.

> Why would it not be a function?

What is the type of its first argument? IIRC, in Lean, it is only a function when a specific universe is given (implicitly).

I'd agree that people are generally going to be less familiar with type theory (though I think it's not uncommon to touch on the simply typed lambda calculus in undergrad courses), but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it (though maybe you meant that you immediately started writing specifications of large, real-world systems in TLA+, but I'd presume you'd then be the outlier on that). In my experience people pick up Isabelle (/HOL) really quickly and writing specifications in a type theory based proof assistant isn't a huge jump from that.

Now, writing actual proofs is a completely different matter, but I didn't disagree with you on how economical/ergonomic the over all approach actually is, just the basic complexity of the theory/specifications ;)

>What is the type of its first argument?

Some universe U, which is an implicit argument. You could alternatively write your Lean example as

def id {u} {α : Sort u} (a : α) : α := a

Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you?

Similar to how one could make those generics explicit, it is actually possible to define a special type of all universes (not including itself). Agda does this by having a special primitive type of universe levels. As an example

id : forall {u : Level} -> forall {A : Set u} -> A

is the signature of the universe polymorphic identity function. The Level type doesn't you any issues because it is essentially a 'top' type that doesn't have a type itself.

> but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it

That has not been my experience. Typed formalisms have further complications with "partial" functions -- either they're actually partial, which is a rather complex concept, or you need refinement types to define them, as well as with constructive mathematics, which isn't necessary for specification. Plus, what are you going to do with your specifications after a few hours if you can't write proofs after few hours (or a few days)? And because of that the tutorials don't and won't just teach specification first and proof later -- as the TLA+ tutorials do -- so even if this were hypothetically true, you have nowhere to learn things like that. Lean has very good tutorials, and you can compare how far they get how quickly with the TLA+ tutorials. I don't know if it's even possible to teach such formalisms the same way as TLA+, but even if it were possible, I haven't seen such tutorials. Those languages are so infused with their formalism's proof theory that it's hard to separate the two [1]. For example, most typed formalisms define integer division by zero to equal zero. Suppose they didn't, and they wanted to teach how to define division "properly". How much would a student need to know in order to define and use the div function? OTOH, TLA+ handles partiality in what I think is a simpler way, with a careful definition of Hilbert's epsilon operator (see https://pron.github.io/posts/tlaplus_part2#the-choose-operat...)

Finally, most specifications people in industry are interested in are not of sequential algorithms but concurrent ones, which you also can't do after a few hours (or a few days).

> In my experience people pick up Isabelle (/HOL) really quickly

Depends what you mean by "really quickly." Isabelle has some accidental complications such as the nested languages. But I think something like Why3 can be picked up quickly, although it doesn't handle concurrency easily.

> Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you?

The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions. I call them subroutines, but those that call them functions know (I hope) that they're overloading the term. In any event, students that do learn simply typed lambda calculus learn it in the context of programming languages whose type systems are inconsistent and they certainly don't learn how to do maths with them.

Anyway, `id` is not a function in Lean because the universe argument doesn't have a type. But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox?

[1]: Which I think is a big problem. The clean separation of model and proof is an important property of a formal logic designed for ease of learning, expression and comprehension, and we must not forget that ease of learning, expression, and comprehension -- so that practitioners rather than logicians will be able to make everyday use of it -- has been a central goal of formal logic since at least Frege, if not Boole or even Leibniz, equal in importance to, if not superseding, that of mechanical proof. I might be getting carried away, but I think that TLA+ is a pretty special accomplishment in the history of formal logic in that it is perhaps the first truly rich formal logic that is commonly used by non-specialist practitioners in their day-to-day work.

If you're fine with 'stupid' refinement types in the form of subset types without coercion, not only do you get them 'for free' from the core type theory without introducing another language element, I personally also think they're quite intuitive. Using a subset type of non-zero nats or providing a proof that the argument isn't zero to define a 'proper divsion' just 'makes the most sense' in my opinion, but that may just be ultimately down to personal taste.

I really do think though that no single part of dependent type theory is actually all that complex. It's not as simple as TLA+, but there's nothing really hard about it till you start proving.

And I'm not saying that all this is feasible right now, but I'm fairly certain that this is at least fundamentally possible. You can't 'truly' separate specifications from proofs in dependent type theory, but you also definitely don't need to really understand how to write actual proofs to write even complex specifications in it. All of this of course depends on stronger automation for a good subset (possibly by also integrating strongly with other provers), but I don't think that's a total pipe dream (though I am definitely personally biased on this).

>The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions

I'm just talking about the 'well-behaved' subset, but let me go at this from another angle.

If Lean tomorrow introduced a Sort Omega to type universes, the set of programs that you can write wouldn't change. It's essentially just a syntactic change. Would that really be enough to make you say that these are functions now while they previously weren't?

>But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox?

If you quantify over a universe, a constraint gets introduced as part of the type checker. These constraints can be viewed as a graph that is checked for cycles, so not having a specific universe isn't an issue.

> but I don't think that's a total pipe dream

You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages.

> Would that really be enough to make you say that these are functions now while they previously weren't?

Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe.

> so not having a specific universe isn't an issue.

Does that require forbidding full recursion, or can you still introduce non-computable objects?

>Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe.

That's true, but I don't think you necessarily need a type for all universes (excluding itself), just some other way to denote that type is supposed to be universe polymorphic.

>Does that require forbidding full recursion, or can you still introduce non-computable objects?

I'm not sure what you mean exactly. The core type theory assumes that all functions are terminating. You can 'cheat in' full recursion by providing a non-computational termination proof, but the type checker would still be assuming that its actually terminating.

I think if that wasn't the case, it'd need to be restricted (unless you did something really weird like introducing infinite negative universe levels).