[HN Gopher] The Hitchhiker's Guide to Logical Verification [pdf]
       ___________________________________________________________________
        
       The Hitchhiker's Guide to Logical Verification [pdf]
        
       Author : nextos
       Score  : 48 points
       Date   : 2024-07-30 17:51 UTC (5 hours 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.
        
         | 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.
        
       | FranklinChen wrote:
       | There's also a 2024 edition
       | https://github.com/blanchette/interactive_theorem_proving_20...
        
       ___________________________________________________________________
       (page generated 2024-07-30 23:00 UTC)