[navaati]

And yet Agda, which is a proof language, was included (in the ML family).

Looking at some TLA+ examples, I’d say, squinting a bit… somewhere around Prolog ? I’d love to hear someone chip in !

[colanderman]

Yes, having used both TLA+ and Prolog extensively, they share many similarities (both having roots in first-order logic). In practice -- TLA+ code is often a bit more "imperative" owing to the fact that unbounded existential quantification isn't implemented in the TLC interpreter (whereas in Prolog, it is a core aspect of any interpreter).

And of course, TLA+ has a suite of temporal operators used exclusively for declaring contracts in service of its role for verifying specifications. Which (as @hwayne points out elsewhere) stem from mathematics -- Linear Temporal Logic specifically -- and not programming.

[Warwolt]

Eh, even though you prove things about your specs (possibly) there's still a difference between proof assistances and spec languages