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