[tlarkworthy]

I am not convinced.

There is no justification for specification languages to insist on a single global namespace with no option for namespacing. Just coz an operator doesn't compose does not undermine the usefulness that some things do compose, and that namespacing and scopes are generally useful organisation and communication techniques.

The only reason why LTL is in a global namespace is pure legacy inertia. Academics only apply it to toy problems, so it never needs the scaling features like namespacing.

Its not about logic. Thats just post-hoc stockholm syndrome.

[dan-robertson]

I don’t understand this at all. Either you have a totally different definition of namespacing to me (For me, this is basically getting to write x in most places and Foo::x and Bar::x in some places instead of foo_x and bar_x everywhere), or you’re just not addressing any of the issues discussed in the article (fairness, liveness, framing, etc).

[tlarkworthy]

Look at the 2nd paragraph of the motivating conversation:

``` 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.

[dan-robertson]

I think the point of the article isn’t that you don’t have namespaces (which are basically trivial) but that, given two names, you can’t often combine them into something that gives you what you want. Instead you need to tease apart their definitions and combine them in a more complicated way. And it is this problem that the article is about

[ahelwer]

Can you describe how a formal specification system with namespacing would work?

[kgwxd]

Clojure Spec has it https://clojure.org/about/spec#_global_namespaced_names_are_...

[gugagore]

To me Clojure Spec is more like IDL or a JSON Schema (or CBOR or Protobuf or etc), but with more "dynamic" stuff as opposed to just sum/product types.

It doesn't occupy the same space as, say, TLA+.

[hwayne]

Clojure Spec is a contract system, which is a common way to write code specifications. You can formally verify it in theory; ACL2, another lisp, is used in formal verification. It's also hard to compose formally-verified code, as Lars talks about in the original link.

[gugagore]

Thanks for the correction. I've wanted to see more examples of Clojure Spec in practice because I had really understood it as an interface description language.

[tlarkworthy]

Something equivalent to hierarchical state machines.