Errors are not the same as incorrectness

Program checkers, if they are to check objective properties rather than the prejudices of their authors, must ground their judgements in some aspect of programs' behavior. (Or in their maintainers' behavior, but that's much harder to prove anything about.) Usually the property they check is whether the program will have errors at runtime. If it will fail dynamically, then the checker judges it a bad program statically.

This is an obvious premise, and it's the standard justification for all sorts of program checking, but it's not necessarily true, as Andreas Rossberg points out:

Take the following degenerate program for computing travel routes:

ComputeAndDisplayTravelRoute(inputs);
"boo" - 1;

This will throw a type error on the second line, and a tool like Dialyzer would (correctly) diagnose that (it's obviously trivial in this case). However, before this error is raised, the program actually successfully completes its designated job, namely computing a travel route and displaying it to the user. Yet such a program is defined as "invalid". I'm asking why.

Crashing on exit is a fairly common problem. (Games seem particularly prone to this, perhaps because graphics has so much hardware-dependent setup and teardown.) It doesn't usually cause any problem for the user, so it's not a high priority to fix. But the usual standard of program checking considers it unforgiveable.

Programs that produce errors (of any kind, not just type errors) are usually much worse than programs without. But not always. The properties we check are only an approximation to the ones we care about.

2 comments:

  1. So what is a complete program? Candidates: a function, a module, a binary, a system image... Typed Racket makes it explicit that a module is checked. Not all languages have such a clear opinion about this.

    ReplyDelete
  2. Re: "The properties we check are only an approximation to the ones we care about."

    As noted in "types considered harmful" by Benjamin Pierce (author of TAPL), attempting to prove any non-trivial property about a program will catch a lot of errors, including many errors for which we aren't specifically searching. Thus, perhaps it doesn't really matter which properties we check, so long as we check enough properties to find the errors.

    ReplyDelete

It's OK to comment on old posts.