[scotty79]

All this is saying is you can't compose behaviors because we insist on having only one whole state, and only one concept of what 'next' state is.

If you can have state with sub-states and 'next' operator that is respective to what sub-state we want to address then this example is easily composable.

But then of course you might want to have substates interact with each other so it complicates further. It just looks like multithreaded programming.

[Pet_Ant]

Sure but do you have formal model of such a system that is sound? I think unstated is that LTT is a known, intuitive, and well understood model. Sure you can ad hoc a fix but will it have any rigor?

[scotty79]

That's the trade-off. Either you have things simple or expressive.

But I'm strong supporter of approach where you start with the semantics you want and work hard to make it work as opposed to simple to implement semantics you don't want because it makes programming harder.

I prefer TypeScript approach than C++ one.

[hwayne]

Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.

[scotty79]

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.

[hwayne]

I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java.

Switching to a different notation helps with some of the practical details, but doesn't remove the essential problems that arise in composing specs.

[scotty79]

The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.

[Pet_Ant]

It must be sound or it's of no use. Reminds me of the Ultraviolet Catastrophe. They had a theory that gave them precise answers, they just happened to be blatantly wrong.

[scotty79]

Unsound things can be useful. https://frenchy64.github.io/2018/04/09/unsoundness-reply.htm...