[HN Gopher] The Hitchhiker's Guide to Logical Verification [pdf]...
___________________________________________________________________
The Hitchhiker's Guide to Logical Verification [pdf] (2023)
Author : nextos
Score : 84 points
Date : 2024-07-30 17:51 UTC (1 days ago)
(HTM) web link (browncs1951x.github.io)
(TXT) w3m dump (browncs1951x.github.io)
| layer8 wrote:
| Actual source, which also provides an alternative PDF suitable
| for smaller screens:
| https://github.com/blanchette/logical_verification_2023
| kragen wrote:
| thanks! that version also doesn't have a license
| nextos wrote:
| 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).
|
| _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.
| didericis wrote:
| > Anything else worth knowing?
|
| K framework
|
| https://runtimeverification.com/blog/k-framework-an-overview
| nextos wrote:
| Thanks, I meant other Lean resources. This is also
| interesting, though.
| steego wrote:
| K Framework is very interesting.
|
| 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.
| didericis wrote:
| > Sorry for the long post.
|
| 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.
| steego wrote:
| It really is and I'm glad you appreciated it.
|
| 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.
| 082349872349872 wrote:
| _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 O2 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.
| nickpsecurity wrote:
| Building High Integrity Applications with SPARK
|
| https://www.amazon.com/Building-High-Integrity-Applications-...
|
| That will be more practical than most works on formal
| verification.
| LiamPowell wrote:
| Also: https://www.adacore.com/books/implementation-guidance-
| spark
| FranklinChen wrote:
| There's also a 2024 edition
| https://github.com/blanchette/interactive_theorem_proving_20...
| ChrisArchitect wrote:
| (2023)
|
| Official link: https://lean-forward.github.io/hitchhikers-
| guide/2023/
___________________________________________________________________
(page generated 2024-07-31 23:02 UTC)