3 ms·

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

• kgwxd 6y ago
  Clojure Spec has it https://clojure.org/about/spec#_global_namespaced_names_are_more_important https://clojure.org/about/spec#_global_namespaced_names_are_...
  • gugagore 6y ago
    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 6y ago
      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 6y ago
        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 6y ago
  Something equivalent to hierarchical state machines.