[HN Gopher] Three ways formally verified code can go wrong in pr...
       ___________________________________________________________________
        
       Three ways formally verified code can go wrong in practice
        
       Author : todsacerdoti
       Score  : 29 points
       Date   : 2025-10-12 06:17 UTC (16 hours ago)
        
 (HTM) web link (buttondown.com)
 (TXT) w3m dump (buttondown.com)
        
       | jonathanstrange wrote:
       | No hardware failure is considered? No cosmic rays flipping bits?
       | No soft or hard real-time guarantees are discussed? What about
       | indeterminate operations that can fail such as requesting memory
       | from some operating system dynamically?
       | 
       | I'm asking because I thought high integrity systems are generally
       | evaluated and certified as a combination of hardware and
       | software. Considering software alone seems pretty useless.
        
         | codebje wrote:
         | Specifications that are formally verified can definitely cover
         | real-time guarantees, behaviour under error returns from
         | operations like allocation, and similar things. Hardware
         | failures can be accounted for in hardware verification, which
         | is much like software verification: specification + hardware
         | design = verified design; if the spec covers it, the
         | verification guarantees it.
         | 
         | Considering software alone isn't pretty useless, nor is having
         | the guarantee that "inc x = x - 1" will always go from an Int
         | to an Int, even if it's not "fully right" at least trying to
         | increment a string or a complex number will be rejected at
         | compile time. Giving up on any improvements in the correctness
         | of code because it doesn't get you all the way to 100% correct
         | is, IMO, defeatist.
         | 
         | (Giving up on it because it has diminishing returns and isn't
         | worth the effort is reasonable, of course!)
        
         | westurner wrote:
         | Side channels? Is best out of 2 sufficient or is best out of 3
         | necessary?
         | 
         | From https://news.ycombinator.com/context?id=39938759 re:
         | s2n-tls:
         | 
         | > [ FizzBee, Nagini, Deal-solver, Dafny; icontract,
         | pycontracts, Hoare logic, invariants, parallelism and
         | concurrency and locks, io latency, pass by reference in
         | distributed systems, "FaCT: A DSL for Timing-Sensitive
         | Computation" and side channels [in hw and software]
         | https://news.ycombinator.com/item?id=38527663 ]
         | 
         | There are so many things to consider;
         | 
         | /? awesome-safety
         | https://westurner.github.io/hnlog/#search:awesome-safety :
         | 
         | awesome-safety-critical: https://awesome-safety-
         | critical.readthedocs.io/en/latest/
         | 
         | Hazard (logic) https://en.wikipedia.org/wiki/Hazard_(logic)
         | 
         | Hazard (computer architecture); out-of-order execution and
         | delays:
         | https://en.wikipedia.org/wiki/Hazard_(computer_architecture)
         | 
         | Soft error: https://en.wikipedia.org/wiki/Soft_error
         | 
         | SEU: Single-Event Upset: https://en.wikipedia.org/wiki/Single-
         | event_upset
         | 
         | And then cosmic ray and particle physics
        
       | ip26 wrote:
       | Is asserting the assumptions during code execution not standard
       | practice for formally verified code?
        
         | ngruhn wrote:
         | How would that look like if you accidentally assumed you have
         | arbitrary large integers but in practice you have 64 bits?
        
           | appellations wrote:
           | Add(x,y):            Assert( x >= 0 && y>= 0 )             z
           | = x + y             Assert( z >= x && z >= y )
           | return z
           | 
           | There's definitely smarter ways to do this, but in practice
           | there is always some way to encode the properties you care
           | about in ways that your assertions will be violated. If you
           | can't observe a violation, it's not a violation
           | https://en.wikipedia.org/wiki/Identity_of_indiscernibles
        
         | cowsandmilk wrote:
         | That's impractical. Take binary search and the assumption the
         | list is sorted. Verifying the list is sorted would negate the
         | point of binary search as you would be inspecting every item in
         | the list.
        
           | AnimalMuppet wrote:
           | Only if you verify it for every search. If you haven't
           | touched the list since the last search, the verification is
           | still good. For some ( _not_ all) situations, you can verify
           | the list at the start of the program, and never have to
           | verify it again.
        
           | voxl wrote:
           | ASSERTING the list is sorted as an assumption is
           | significantly different form VERIFYING that the list is
           | sorted before executing the search. Moreover, type systems
           | can track that a list was previously sorted and maintained
           | it's sorted status making the assumption reasonable to state.
        
       | skybrian wrote:
       | Many interesting statements aren't a property of the code alone.
       | They're a property of the code when it's run in a particular
       | environment. If you want the proof to be portable then it should
       | only make assumptions that are true in any environment.
        
       | rook_line_sinkr wrote:
       | I got told to use these words back in uni
       | 
       | verification - Are we building the software right?
       | 
       | validation - Are we building the right software?
       | 
       | makes many a thing easier to talk about at work
        
       ___________________________________________________________________
       (page generated 2025-10-12 23:00 UTC)