[syrak]

Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually the original meaning of it afaik, and then I went to look for a source for it and that grew into this whole blogpost.

[steego]

First of all, thank you for writing that up!!!

Disclaimer 1: I have the same last name as Burstall's collaborator, Joseph Goguen. If we're related, it's VERY distant, so I truly can't add anything.

Disclaimer 2: I'm going to tie this back into algebras.

Setup 1: However, I have been a little obsessed with Burstall and Goguen lately and I've been SLOWLY working through some papers and trying to make sense of it. I'm just an F# programmer who likes languages, not an academic.

Setup 2: I've known about Burstall/Goguen for some time, but I never understood the gravity of their respective work until recently. And I have quite literally been annoying with my tech friends and family with all my "Oh my god!" moments as I've been going papers and festschrifts.

This whole time, I haven't been sure if I've been interpreting what I'm reading correctly, so your post has been wonderful in settling some of that.

I understand that some people may resist the idea of describing algebraic data types as analogous to the fundamental theorem of arithmetic for types. Burstall and Goguen were motivated by creating tools and systems built on solid foundations, such as universal algebras, to utilize analytical tools like logic systems and category theory for deeper insights.

However, I believe they were particularly focused on how algebraic data types model the cardinality of state spaces and transitions between states for this reason:

They were designing a specification system that helped working programmers design systems accomplish two things (In today's parlance):

1. Make invalid states impossible. 2. Make invalid transitions between states impossible.

While learning Maude (OBJ's successor), I've been particularly fascinated with how its parent language let you define very fine grained domains.

And it makes sense, because if you're going to search through that domain to find counter-examples violating your theories, it makes sense to reduce the search space proactively.

But what really drove that for me (and maybe I'm projecting here), is how that seemed to correspond to a little program I wrote that constructed a bijection between the natural numbers and all closed lambda functions.

https://gist.github.com/sgoguen/46200419194eb29b82079b0804e5...

But what really convinces me that they had that in mind is how Maude and OBJ let you add attributes to constructors to identify them as associative or commutative or whether it has an "id" where the impact of these attributes on the constructors actually reduces the state space.

Again, I could be projecting here, but I would love to hear your thoughts and I am excited to read your next post!

Thank you!

[syrak]

I learned a lot from this and your other comment here!

The way I connected the dots when I read about Clear (and OBJ) is that it let me explain free algebras by example, by just showing Clear code. That hopefully makes the concept more accessible than the dry mathy definitions that would have the eyes of most readers glaze over.

I must say that I'm not familiar with Burstall and Goguen's line of research beyond what I've written so far. In the future I'd especially like to know what lessons these specification languages can teach (or already taught) about ML-style module systems, OO languages, and formalizations of mathematical structures in proof assistants (Clear reminds me of the little I've seen of Hierarchy Builder in Coq).

One concrete question I have is how Clear or OBJ or Maude code is actually meant to be run. Your description of these languages reminds me of model checking tools like TLA+/Alloy. Does Maude target a similar niche?

[steego]

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.