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