[cap-talk] C vs. Safety

[David Wagner]

Baldur writes:
>Hmm... isnt static safety as unsolvable as the famous halting problem?
>That is the question: does program p ever do anything unsafe?

There is a standard trick, whenever you run into something that smells
like the halting problem.  We put the burden on the programmer to write
code that is manifestly safe.  If it isn't clear whether the code is safe,
we tell the programmer: go rewrite your code until it is clear why it
is safe, or go add annotations that make it clear why the code is safe.
I see no reason to think that this standard trick cannot be applied here.

For instance, think about your compiler's type-checker.  Suppose we
wanted to be really sure that the programs we write do not try to add
a string to a number, because this would cause them to crash.  It is
undecidable whether an arbitrary program might crash in this way.
However, a type-checker can still ensure that no program you ever run
crashes in this way, by simply refusing to compile programs that don't
type-check (i.e., by rejecting programs where it is not clear whether
the program could crash with this kind of error).  Sure, the compiler
might reject programs that are otherwise perfectly good, simply because
they do not type-check, but it is also rejects many erroneous programs.
For these reasons, type-checking can be useful in practice in preventing
certain kinds of errors, even though in theory it is undecidable to tell
whether a given program contains an instance of that kind of error.

Undecidability isn't nearly so bad as people sometimes think.