What is a type error?

[Marshall]

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) 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.


Marshall