> 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.