What is a type error?

[David Hopwood]

Chris Smith wrote:
> David Hopwood <david.nospam.hopwood at blueyonder.co.uk> wrote:
> 
>>Maybe I'm not understanding what you mean by "complete". Of course any
>>type system of this expressive power will be incomplete (whether or not
>>it can express conditions 3 to 5), in the sense that it cannot prove all
>>true assertions about the types of expressions.
> 
> Ah.  I meant complete enough to accomplish the goal in this subthread, 
> which was to ensure that the compiler knows when a particular int 
> variable is guaranteed to be greater than 18, and when it is not.

I don't think that placing too much emphasis on any individual example is
the right way of thinking about this. What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations, and understanding whether any remaining run-time checks
are guaranteed to succeed.

Look at it this way: suppose that I *need* to verify that a program has
no range errors. Doing that entirely manually would be extremely tedious.
If the compiler can do, say, 90% of the work, and point out the places that
need to be verified manually, then that would be both less tedious, and
less error-prone.

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