4 ms·

The Hitchhiker's Guide to Logical Verification [pdf] (2023)

100 points by nextos 2y ago

layer8 2y ago
Actual source, which also provides an alternative PDF suitable for smaller screens: https://github.com/blanchette/logical_verification_2023 https://github.com/blanchette/logical_verification_2023
- kragen 2y ago
  thanks! that version also doesn't have a license
nextos 2y ago
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 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 2y ago
  > Anything else worth knowing? K framework https://runtimeverification.com/blog/k-framework-an-overview https://runtimeverification.com/blog/k-framework-an-overview
  - nextos 2y ago
    Thanks, I meant other Lean resources. This is also interesting, though.
  - steego 2y ago
    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 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 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 2y ago
      > 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 2y ago
- nickpsecurity 2y ago
  Building High Integrity Applications with SPARK https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-... That will be more practical than most works on formal verification.
  - LiamPowell 2y ago
    Also: https://www.adacore.com/books/implementation-guidance-spark https://www.adacore.com/books/implementation-guidance-spark
- indolering 2y ago
  IELE: basically WASM but designed for formal verification. But I think it's dead.
FranklinChen 2y ago
There's also a 2024 edition https://github.com/blanchette/interactive_theorem_proving_2024 https://github.com/blanchette/interactive_theorem_proving_20...
deleted 2y ago
[deleted]
ChrisArchitect 2y ago
(2023) Official link: https://lean-forward.github.io/hitchhikers-guide/2023/ https://lean-forward.github.io/hitchhikers-guide/2023/

100 points by nextos 2y ago

Actual source, which also provides an alternative PDF suitable for smaller screens: https://github.com/blanchette/logical_verification_2023 https://github.com/blanchette/logical_verification_2023

kragen 2y ago
thanks! that version also doesn't have a license

nextos 2y ago

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 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 2y ago
> Anything else worth knowing? K framework https://runtimeverification.com/blog/k-framework-an-overview https://runtimeverification.com/blog/k-framework-an-overview
- nextos 2y ago
  Thanks, I meant other Lean resources. This is also interesting, though.
- steego 2y ago
  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 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 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 2y ago
    > 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 2y ago
nickpsecurity 2y ago
Building High Integrity Applications with SPARK https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-... That will be more practical than most works on formal verification.
- LiamPowell 2y ago
  Also: https://www.adacore.com/books/implementation-guidance-spark https://www.adacore.com/books/implementation-guidance-spark
indolering 2y ago
IELE: basically WASM but designed for formal verification. But I think it's dead.

FranklinChen 2y ago

There's also a 2024 edition https://github.com/blanchette/interactive_theorem_proving_2024 https://github.com/blanchette/interactive_theorem_proving_20...

deleted 2y ago

[deleted]

ChrisArchitect 2y ago

(2023) Official link: https://lean-forward.github.io/hitchhikers-guide/2023/ https://lean-forward.github.io/hitchhikers-guide/2023/