What is a type error?

[Chris Smith]

Marshall <marshall.spight at gmail.com> wrote:
> David Hopwood wrote:
> > Marshall wrote:

> > > 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) 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. On the
> other hand the points you raise are good ones, and affect
> the usability of the language.

There doesn't seem to be a point of disagreement here.  Programmers 
often need to require certain properties to be checked at compile-time.  
Others could go either way.  There is no property that a program would 
rationally desire to *require* be checked at runtime; that would only 
occur because the compiler doesn't know how to check it at compile time.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation