[HN Gopher] How to train your program verifier
       ___________________________________________________________________
        
       How to train your program verifier
        
       Author : matt_d
       Score  : 76 points
       Date   : 2026-02-18 21:10 UTC (5 days ago)
        
 (HTM) web link (risemsr.github.io)
 (TXT) w3m dump (risemsr.github.io)
        
       | woodruffw wrote:
       | At a very quick look, no evidence is given that the "bugs" found
       | in requests are in fact reachable, i.e. not prevented by
       | construction. And sure enough, the very first one is impossible
       | because of a validating guard[1]: `address_in_network` only gets
       | called after `is_valid_cidr`, which enforces the presence of a
       | slash.
       | 
       | I think we should hold claims about effective static analysis
       | and/or program verification to a higher standard than this.
       | 
       | [1]:
       | https://github.com/psf/requests/blob/4bd79e397304d46dfccd76f...
        
         | JimDabell wrote:
         | > the very first one is impossible because of a validating
         | guard[1]: `address_in_network` only gets called after
         | `is_valid_cidr`, which enforces the presence of a slash.
         | 
         | It's correct to flag this code. The check is performed manually
         | outside of the function in question. If you call the function
         | directly, the bug surfaces.
         | 
         | There is no mention in the function documentation of the
         | validation requirement, making it easy to call incorrectly.
         | Also, if it is required to call the validator before calling
         | this function, then the function could just call it itself.
         | 
         | In short, it's possible to make this code safe by definition,
         | but instead it relies upon the developer to always make the
         | undocumented right choices every single time it is called. I
         | would expect something more rigorous from verified code.
        
           | sebastianmestre wrote:
           | > I would expect something more rigorous from verified code.
           | 
           | I think you just want the illusion of safety :p
           | 
           | A big advantage of verified code is that it enables you to
           | write the sketchy and dangerous-looking code BECAUSE it's
           | proven correct
           | 
           | In fact, skipping as many safety checks as possible is highly
           | desirable. For performance, yes, but also because it's less
           | code to maintain.
           | 
           | Our tools already do this to some extent, for performance.
           | E.g. compilers that remove your bounds or type checks in the
           | generated code when it can prove it's not needed.
        
           | woodruffw wrote:
           | > It's correct to flag this code. The check is performed
           | manually outside of the function in question. If you call the
           | function directly, the bug surfaces.
           | 
           | No, that's just called a precondition. I'm not aware of a
           | single program that doesn't have functions like these,
           | particularly internal APIs.
           | 
           | (It should go without saying, but it's not even an _issue_ in
           | this case: it'll cause an IndexError, but so will thousands
           | of other APIs. Python very explicitly doesn't have exceptions
           | in its type contract; anything can always raise anything.)
           | 
           | > I would expect something more rigorous from verified code.
           | 
           | Nobody said that requests is "formally verified." The only
           | place where that claim is made is in the AI-generated blog
           | post above.
        
         | mistrial9 wrote:
         | clever, but no.. I agree that it is useful and appropriate to
         | flag this section for attention.
         | 
         | I am concerned that the civilian population will be deprived of
         | the benefits of this tech while hyper-competitive formal groups
         | scoop up the talent needed to develop these..
        
       | saithound wrote:
       | What if you asked your favorite AI agent to produce mathematics
       | at the level of Vladimir Voevodsky, Fields Medal-winning,
       | foundation-shaking work but directed toward something the
       | legendary Nikolaj Bjorner (co-creator of Z3) could actually use?
       | 
       | Well, you'd get this embarrassing mess, apparently.
        
         | geraneum wrote:
         | That's because they didn't add "and don't make mistakes!".
         | 
         | And yes, the exclamation mark matters!
        
       | grey-area wrote:
       | I miss the days when humans submitted things they had done to
       | this site, instead of generating long slop articles in 5 minutes:
       | 'LLM-based code synthesis--while mind-numbingly effective--'
       | about slop code they generated in 5 minutes (or worse in hours)
       | with foolish prompts:'Produce mathematics at the level of
       | Vladimir Voevodsky, Fields Medal-winning, foundation-shaking
       | work'.
       | 
       | Should we even read this or should we get an LLM to summarise it
       | onto a few bullet points again?
       | 
       | This bit was interesting in illuminating the human authors'
       | credulity (assuming they believe in their own article):
       | 
       | 'The central move was elegant: stop asking only "is the system
       | safe?", start asking "how far is it from safety?"'
       | 
       | This ersatz profundity couched in a false opposition is common in
       | generated text - does it have anything at all to do with the code
       | generated or is it all just convincing bullshit?
        
       ___________________________________________________________________
       (page generated 2026-02-23 23:01 UTC)