[HN Gopher] Benchmarking Crimes Meet Formal Verification
       ___________________________________________________________________
        
       Benchmarking Crimes Meet Formal Verification
        
       Author : snvzz
       Score  : 28 points
       Date   : 2025-05-19 00:04 UTC (3 days ago)
        
 (HTM) web link (microkerneldude.org)
 (TXT) w3m dump (microkerneldude.org)
        
       | Animats wrote:
       | Sigh.
       | 
       | Decades ago I headed a project to build a proof of correctness
       | system.[1] It was for a rather dialect of Pascal for real-time
       | engine control programs. Some of the comments I made back then
       | still apply.
       | 
       | - Assertions belong in the program source, and in the same syntax
       | as the language of the program. They're mostly written by the
       | people writing the code. The proof of correctness work can and
       | should be integrated with development.
       | 
       | - Most, but not all, of the theorem proving can be automated with
       | what's now called a "SAT solver". We had the original Oppen-
       | Nelson simplifier for that.
       | 
       | - Sometimes you need more theorem proving power than a SAT
       | solver. We used the original Boyer-Moore theorem prover for that.
       | It's automatic, but you can help it by suggesting intermediate
       | theorems.
       | 
       | - To tie complex theorems to concrete code, programmers should
       | write                   assert(a);         assert(b);
       | 
       | where a can be proved from the code above by the SAT solver, and
       | b is what you need to prove constraints on the following code.
       | Now you have to prove a implies b. That's when you need a more
       | interactive prover, or one with more power. a implies b should be
       | a statement that stands alone, without reference to other code.
       | This allows turning the problem over to the people who are into
       | theorem proving, while the programmers can get on with coding.
       | 
       | - Many of the people involved in program verification are heavily
       | into the formalism, rather than seeing this as a way to eliminate
       | bugs. This leads to excessive formalism. That tendency has to be
       | restrained.
       | 
       | [1] https://github.com/John-Nagle/pasv
        
         | staunton wrote:
         | Was that project a success? Was it used in practice? Was the
         | effort justified by any usages?
         | 
         | The repository readme doesn't seem to go into that.
        
           | Animats wrote:
           | It was used a little, but the actual code that shipped in the
           | engine controller was not written in Pascal-F, because the
           | compiler generated inefficient code.
        
         | MaxBarraclough wrote:
         | > Assertions belong in the program source, and in the same
         | syntax as the language of the program. They're mostly written
         | by the people writing the code. The proof of correctness work
         | can and should be integrated with development.
         | 
         | SPARK Ada takes this approach, what do you make of it?
        
       ___________________________________________________________________
       (page generated 2025-05-22 23:01 UTC)