Lean is quite nice, but last time I checked this was the only software verification-oriented book. Anything else worth knowing?
Most work in Lean is geared towards mathematics, in contrast to Isabelle and Coq. Actually, The Hitchhiker's Guide is a rewrite of Concrete Semantics (Isabelle).
On its surface, you could say it’s a language and toolset for language designers to implement languages and construct formal proofs of your language’s semantics.
The underlying semantics for this language is based on something called matching logic, which defines a system of logic, not for true and false statements, but pattern matching expressions where true corresponds to “matches everything” and false corresponds to “match nothing”.
The craziest part of K Framework is how so many of the fundamentals ideas go back to the 70s in a language called OBJ.
What you have to understand is OBJ was this language was inspired by the collaboration and lifetime friendship between Rod Burstall and Joe Goguen, who was a category theorist working on defining algebraic data types.
They laid the foundation to create a formal specification language, that let you construct abstract data types, mathematical objects, systems of logic and domain specific languages in a REPL environment. They also formalized what a system of logic was in category theory and then used THAT as the semantic foundation for their new language.
OBJ influenced all sorts of languages like ML, C++, Haskell, Coq, and even the Lean language itself.
So when I say K Framework has roots, those roots really go back to a family of logic based languages that have been living in relative obscurity for decades, but is now finding itself well positioned to solve many new interesting applications.
IMO, OBJ and Maude (based on OBJ) are like the Lisps of category theory based languages, especially after looking at how Maude is defined in Maude.
Sorry for the long post. I’ve been exploring this history for months and I’m still floored by OBJ.
No need at all. I'm very interested in this area too, but didn't know all the OBJ lore. I got into this kind of thing after learning about Hilbert's program, which goes all the way back to the late 1800s. The history of formal logic in general is incredibly deep/very very interesting.
Logicomix: An Epic Search for Truth (2009) hints that pushing formal logic forward may be as attractive, yet dangerous, for mental health as ascending Everest without supplemental O₂ is for physical:
Weave a circle round them thrice,
And close your eyes with holy dread
For they on honey-dew hath fed,
And drunk the milk of Paradise.
I love these stories and how you can show the lasting impact that these very direct and personal influences had on the tools we use today.
I recently learned that Burstall met Peter Landin and Christopher Strachey through this underground study group forms by a gentleman named Mervyn Pragnell, who skulked around in book shops so he could invite people who were reading books on logic to his group where they would study lambda calculus together.
To think a meetup organizer in the early 60s had this lasting impact that carries to today.
