P.S. 1. The very large Coq/Agda texts are usually large because of the proofs, not the specification/propositions. There's a 5-10x ratio, if not more. 2. I do

P.S. 1. The very large Coq/Agda texts are usually large because of the proofs, not the specification/propositions. There's a 5-10x ratio, if not more. 2. I don't think that TLA+'s theory is intrinsically more "straightforward" than Agda's, even though it's certainly more familiar (I know some people who would insist that type theory is more straightforward than set theory). I think that a lot of work has gone into making TLA+ relatively easy to grasp; I think it's more design than a specific choice of theory, although the choice of theory certainly affects the design. In addition, as I've already mentioned, I think that TLA itself (i.e. not the set theory in the "+") is a particularly beautiful theory for talking about computation and discrete systems, that has some obvious advantages over the lambda calculus; in particular the abstraction/refinement relation that's the core of TLA (the semantic domain of TLA is a Boolean lattice where the less-than relation is behavior refinement).