Hacker News Reader

Comment by chrisseaton | Hacker News Reader

I think that's why you're getting the response you are in this thread - if it really did '100% of the positives with 0% negatives', it'd have to consider the logic. There's an impossibility proof for that which has already been cited in the thread. It's usually illustrated using a function that solves the halting problem rather than the Goldbach conjecture.

If the compiler rejects things that have free appear twice on branching control flow paths but aren't actually broken due to dynamic control flow (like your looping example given elsewhere) then that's a false positive, isn't it?

And people thought '0% negatives' was meaning 'no false positives'.

View on HN

I see your point, and it's a valid criticism of my statement. I meant it more in the sense that the static checkers I have used would use hackish ad-hoc heuristics which did not work very well, and gets constantly tweaked by the implementor.

The D implementation, in contrast, uses a well-defined rule outlined above, and it works predictably and reliably (absent implementation bugs, rather than ad hoc rule shortcomings).

Another way of putting it is that the rules of the language are changed to make 0%/100% results workable. The compiler never says "there may be a problem here". It passes or is rejected. If it is passes, it is memory safe.

That approach is a really good point in the design space IMO. It is also the tradeoff that people have to make when designing type systems. Many programs are correct but rejected by their language's type system, but if the language is well designed it was probably a really weird and unintuitive program to begin with, so it's okay to reject it anyway.

For example, consider:

    for (i = 0; i < 10; ++i);

some C compilers issue a warning for the trailing ; as do some static checkers. If the programmer intended that, the warning is a false negative because the C language rules allow it.

However, such a construct is a hard error in D. Whether you meant it or not, it is not allowed. This is what I meant.

A construct in D that would pass is:

    for (i = 0; i < 10; ++i) { }

That would be a false positive, if I am understanding things correctly. The warning is about code that is correct, yet it warns, hence false positive. If the warning was missing for incorrect code that would be a false negative. At least that is the terminilogy used for static analysis.

I think the terms normally used for this is "completeness" and "soundness", as in, the D type system is "sound" because it rejects all programs with use-after-free, but it is "incomplete" because there are some programs that cannot exhibit use-after-free for any input values, but that the type system rejects.

Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.

Reply on news.ycombinator.com