The Hitchhiker's Guide to Logical Verification [pdf] (2023)
browncs1951x.github.io
browncs1951x.github.io
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).
Concrete Semantics is really worth checking out too: http://concrete-semantics.org/concrete-semantics.pdf
I'm optimistic about LLMs in this context, as I think they will reduce the cost of formal methods making them much more practical.
K framework
https://runtimeverification.com/blog/k-framework-an-overview
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”.
There’s even a Lean proof for matching logic.
https://gitlab.com/ilds/aml-lean/MatchingLogic
Also, it seems like matching logic is able to subsume so many other systems of logic:
https://en.m.wikipedia.org/wiki/Matching_logic
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.
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.
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.https://www.amazon.com/Building-High-Integrity-Applications-...
That will be more practical than most works on formal verification.
Official link: https://lean-forward.github.io/hitchhikers-guide/2023/