| I thought the way you explained free algebras was great. I am absolutely not an expert in Clear/OBJ (I'm very much still learning), so I personally appreciated your presentation of it. To answer your question regarding how these languages are meant to be run: 1. You know more about Clear than I do, so I'm at a loss. 2. I've read through OBJ's documentation, but I've never used it. But Goguen is usually demonstrating it as a language for quickly prototyping mathematical objects, experimental programming language, logical systems, theorem provers, etc. The manuals usually focuses on applying reduction rules to verify models (He claims reduction is often the go to method for proving properties), so I'm not entirely sure how much it parallels TLA+/Alloy yet. 3. Maude very much feels like OBJ where they added additional features to give it TLA+/Alloy like features that allow you to check invariants through searching. It's worth pointing out that Maude is very reflective and that many features of Maude are written in Maude on top of a fairly small core based on rewrite logic. It's not unusual that while you're reading the documentation for an LTL checkers or an SMT solver feature, that they'll show you the Maude code that defines that feature. https://maude.lcc.uma.es/maude-manual/maude-manualch12.html#... To answer your question: Maude does targets a similar niche and has been used to verify concurrent applications, distributed systems and protocols, but I really haven't explored that side of it yet. I've mostly been playing with Maude's functional modules and really spent much time with Maude's object-oriented modules which reflect the semantics needed to simulate and verify distributed systems. |