[cap-talk] Midori in The Register

[Jonathan S. Shapiro]

On Wed, 2008-08-06 at 23:05 +0200, Rob Meijer wrote:
> On Wed, August 6, 2008 21:46, Jonathan S. Shapiro wrote:
> > While the idiom you favor is useful, Apache is type-unsafe, because it
> > lacks any automated means of checking and its mechanisms can therefore
> > be bypassed.
> >
> 
> So by this reasoning, if one was to write a program in C or C++, using
> coding standards and constructs geared at type safety, and validate this
> code on not violating the coding standards by way of a code review, the
> code would still be unsafe. But when someone manages to create some
> -pedantic-typeunsafe-errors for gcc or g++ to do the checks the codereview
> did, the exact same source code would instantly be considered safe,
> without a single line of code being changed?

I just knew that somebody was going to go here as soon as MarkM
introduced his automation requirement.

Obviously, the code is safe if the code is safe. Equally obviously, any
implementation of an automated safety check can be broken if that
*implementation* is not formally verified.

The issue here comes down to confidence. When the requirement is for
zero errors, we have overwhelming evidence that human review processes
are low-to-zero confidence approaches. Not only do human reviews
universally fail to spot even simple errors (even in the absence of
malice), they equally universally fail to accurately understand what the
precise criteria for correctness are. This is true because the criteria
are too complex, even in seemingly simple systems.[*]

While the automated system may be wrong, it has the dual advantages of
consistency and unlimited attention span.

So to answer your question: yes, the code might be safe, but no sensible
person should *believe* that it is safe merely because a human reviewer
says so.

Thankfully, memory and type safety properties are not that hard to
check.


[*] The formal type system requirements for the BitC core, which doesn't
yet incorporate by-reference, is a mere 33 pages of light formal math:

  Sound and Complete Type Inference for a Systems Programming Language
  http://www.bitc-lang.org/doc/docs/bitc/complete.pdf

  The BitC Type System and Inference Algorithm: Proofs of Soundness and
  Completeness
  http://www.bitc-lang.org/doc/docs/bitc/c-formal.pdf

Good bathtub reading, especially if your drain stopper is out for
repair.


shap