4 ms·

Nobody said it was easy. If you think verification reduces bugs, then surely you can find a bug in Linux’s unverified TCP parsing?

• Jweb_Guru 4y ago
  Many people have found bugs in unverified parsing routines in the Linux kernel. All I'm asking is for someone to find a single one in one of Microsoft's new parsers. Surely, if specification bugs are just as commonplace as other kinds of programming issues, this shouldn't be too big of a request. I'm mostly just tired of people pretending that formal verification produces buggy software at a rate that is in any way comparable to "ordinary" programming. Empirically, it doesn't, and people who claim it does have scant evidence to back up those claims. Are there specification bugs? Sure. Do they happen at the same rate that bugs in comparable unverified code (let alone C code) occur? Not even close.
  • deleted 4y ago
    [deleted]
  • seoaeu 4y ago
    Yeah, but you haven’t found bugs in the Linux kernel’s TCP parser. Your argument basically boils down to “X is true. If you think I’m wrong, then prove it by <extremely difficult task>” (It turns out that verification does reduce bugs, but the refusal of folks here to audit parsers doesn’t prove anything either way)