No. I haven't left anything. I'm just saying that expecting that useful widespread formal specification language will be something as simple as LTT is wildly optimistic and you should expect that it will rather mirror and encompass the complexities and requirements of actual programming, like necessity of composability.

And it will most likely be somewhere between practical but unsound specification languages and those that come from pure mathematics.