What is a type error?

[David Hopwood]

Marshall wrote:
> David Hopwood wrote:
>>Marshall wrote:
>>
>>>Wouldn't it be possible to do them at compile time? (Although
>>>this raises decidability issues.)
>>
>>It is certainly possible to prove statically that some assertions cannot fail.
>>
>>The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html)
>>tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does
>>this -- although some limitations and usability problems are described in
>><http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>.
> 
> I look forward to reading this. I read a paper on JML a while ago and
> found it quite interesting.
> 
>>>Mightn't it also be possible to
>>>leave it up to the programmer whether a given contract
>>>was compile-time or runtime?
>>
>>That would be possible, but IMHO a better option would be for an IDE to give
>>an indication (by highlighting, for example), which contracts are dynamically
>>checked and which are static.
>>
>>This property is, after all, not something that the program should depend on.
>>It is determined by how good the static checker currently is, and we want to be
>>able to improve checkers (and perhaps even allow them to regress slightly in
>>order to simplify them

.. or improve their performance ..

> ) without changing programs.
> 
> Hmmm. I have heard that argument before and I'm conflicted.
> 
> I can think of more reasons than just runtime safety for which I'd
> want proofs. Termination for example, in highly critical code;
> not something for which a runtime check will suffice.

It is true that some properties cannot be verified directly by a runtime check,
but that does not mean that runtime checks are not indirectly useful in verifying
them.

For example, we can check at runtime that a loop variant is strictly decreasing
with each iteration. Then, given that each iteration of the loop body terminates,
it is guaranteed that the loop terminates, *either* because the runtime check
fails, or because the variant goes to zero.

In general, we can verify significantly more program properties using a
combination of runtime checks and static proof, than we can using static proof
alone. That may seem like quite an obvious statement, but the consequence is
that any particular property is, in general, not verified purely statically or
purely at runtime.

I am not opposed to being able to annotate an assertion to say that it should
be statically provable and that a runtime check should not be used. However,

 - such annotations should be very lightweight and visually undistracting,
   relative to the assertion itself;

 - a programmer should not interpret such an annotation on a particular assertion
   to mean that its static validity is not reliant on runtime checks elsewhere;

 - if the class of assertions that are statically provable changes, then a
   tool should be provided which can *automatically* add or remove these
   annotations (with programmer approval when they are removed).


I'd like to make a couple more comments about when it is sufficient to detect
errors and when it is necessary to prevent them:

 - If a language supports transactions, then this increases the proportion
   of cases in which it is sufficient to detect errors in imperative code.
   When state changes are encapsulated in a transaction, it is much easier
   to recover if an error is detected, because invariants that were true of
   objects used by the transaction when it started will be automatically
   reestablished. (Purely functional code does not need this.)

 - Almost all safety-critical systems have a recovery or safe shutdown
   behaviour which should be triggered when an error is detected in the
   rest of the program. The part of the program that implements this behaviour
   definitely needs to be statically correct, but it is usually only a small
   amount of code.

   Safety-critical systems that must either prevent errors or continue
   functioning in their presence (aircraft control systems, for example) are
   in a separate category that demand *much* greater verification effort. Even
   for these systems, though, it is still useful to detect errors in cases
   where they cannot be prevented. When multiple independent implementations
   of a subsystem are used to check each other, this error detection can be
   used as an input to the decision of which implementation is failing and
   which should take over.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>