``` Lars, 7:53: In software engineering, we have largely figured out modularization. All modern programming languages have some form of module system. You can pull in a module and import its functions anywhere. ```
... and then they write a blog about how this is impossible.
namespace is one trivial part of modularization (avoiding naming clashes). All implementations of LTL I have used do not have it. There is no good reason.
Your mentioning 'fairness' and other concepts that are part of expressing proofs on top of a state evolution system. Yes, the proofs are why we are using LTL, BUT, a good amount of time is spent building the model we wish to prove stuff about. There is no reason the state transitions cannot be namespaced and modularised, and it would save a ton of time, even if we have to express proofs globally of the "tree of state space".
Even on the proof level though, liveliness is a property that demonstrates the system never gets cornered. I am pretty sure that for many systems that will be expressible in general terms for a wide family of interesting systems. So I am pretty sure their argument doesn't hold even at the proof of properties level.
The real reason is abstraction is not something the logicians will get cited on, so it's a waste of their time trying to solve that thankless task. And probably they would not be very good at it anyway.
