← Back to context

Comment by JimDabell

7 hours ago

> 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.

> 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.

> 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.

That doesn't mean there's a problem with the code, only with the documentation. So the article is wrong to call it a "real bug". At most it's poor code style that could theoretically lead to a bug in the future.

There's nothing inherently wrong with a function throwing an exception when it receives invalid input. The math.sqrt function isn't buggy because it fails if you pass it a negative argument.

  • > That doesn't mean there's a problem with the code, only with the documentation.

    I disagree. If the obvious way to use an API is the incorrect way, there is a problem with the code.

    If you must call A each time before calling B, drop A and have B do both things.

    If you must call A once before calling B, make A return a token that you then must pass to B to show you called A.

    As another example, look at https://news.ycombinator.com/item?id=47060334):

    “Two popular AES libraries, aes-js and pyaes, “helpfully” provide a default IV in their AES-CTR API, leading to a large number of key/IV reuse bugs. These bugs potentially affect thousands of downstream projects.”

    Would you call that “poor code style that could theoretically lead to a bug in the future”, too?